proposition: Lemma FT_eq1 : Com_law (axf:=Build_Com_ob (FT_f FT_m0)) (bxg:=Build_Com_ob (FT_f FT_i0)) (FT_t'' o FT_p).
proof: Proof. unfold Com_law in |- *; simpl in |- *. apply Trans with (FT_f FT_m0 o FMor G FT_t'' o FMor G FT_p). apply Trans with ((FT_f FT_m0 o FMor G FT_t'') o FMor G FT_p). apply Trans with (FT_k o FMor G FT_p). apply (Prf_pb1_law2 FT_GP FT_diag1). apply Comp_r; apply (Prf_SSC2_law (s x) FT_k). apply Ass1. apply Comp_l; apply FComp1. Qed.
imports: FSC_inc Comma_proj FAFT_SSC2 Th_Adjoint Pres_Limits Pullbacks1