Думал, я уже все подготовил

и дописываю последнюю главу. Мол, могу уже писать доказательство основной теоремы. Но приглядываясь повнимательней, нет, еще кое-чего не хватает. Почему производный функтор композиции (обратных образов при композиции морфизмов) изоморфен композиции производных функторов? Такие вещи не автоматичны, их доказывать надо.