proposition: Lemma FT_diag4 : FT_Apeps FT_i0 o FT_t =_S FT_Apeps FT_j0 o FT_t' o FT_h'.
proof: Proof. apply Trans with (((FT_Apeps FT_m0 o FT_t'') o FT_p) o FT_t). apply Comp_r; apply FT_diag2. apply Trans with (((FT_Apeps FT_m0 o FT_t'') o FT_q) o FT_t' o FT_h'). apply Trans with ((FT_Apeps FT_m0 o FT_t'') o FT_p o FT_t). apply Ass1. apply Trans with ((FT_Apeps FT_m0 o FT_t'') o FT_q o FT_t' o FT_h'). apply Comp_l; apply (Prf_pb1_law1 FT_P). apply Ass. apply Comp_r; apply Sym; apply FT_diag3. Qed.
imports: FSC_inc Comma_proj FAFT_SSC2 Th_Adjoint Pres_Limits Pullbacks1