proposition: Lemma FT_eq3 : forall i : FT_I, Com_law (axf:=Build_Com_ob (FT_f FT_j0)) (bxg:=Build_Com_ob (FT_f i)) (FT_t' o FT_Apeps i).
proof: Proof. unfold Com_law in |- *; simpl in |- *; intro i. apply Trans with (FT_f FT_j0 o FMor G FT_t' o FMor G (FT_Apeps i)). apply Trans with ((FT_f FT_j0 o FMor G FT_t') o FMor G (FT_Apeps i)). apply Trans with (FT_tau_d o FMor G (FT_Apeps i)). apply (FT_eq_tau i). 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