proposition: Lemma Adj_eq3 : ApAphi ad (f o k) =_S ApAphi ad f o FMor G k.
proof: Proof. apply Trans with (ApAphi ad ((FMor F (Id d) o f) o k)). apply AphiPres. apply Comp_r. apply Trans with (Id (F d) o f). apply Idl1. apply Comp_r. apply FId1. apply Trans with ((Id d o ApAphi ad f) o FMor G k). apply (Adj_eq1 ad (Id d) k f). apply Comp_r. apply Idl. Qed.
imports: NatIso HomFunctor2