proposition: Lemma FT_diag1 : Pullback_eq1 (FMor G FT_t) (FMor G (FT_t' o FT_h')) (FT_f FT_i0) (FT_f FT_j0).
proof: Proof. unfold Pullback_eq1 in |- *. apply Trans with (FT_f FT_j0 o FMor G FT_t' o FMor G FT_h'). apply Trans with ((FT_f FT_j0 o FMor G FT_t') o FMor G FT_h'). apply Trans with h. apply Sym; apply (Prf_SSC2_law (s x) h). apply Trans with (FT_tau_d o FMor G FT_h'). apply Sym; exact H. apply Comp_r. apply (Prf_SSC2_law (s x) FT_tau_d). apply Ass1. apply Comp_l. apply FComp1. Qed.
imports: FSC_inc Comma_proj FAFT_SSC2 Th_Adjoint Pres_Limits Pullbacks1