proposition: Lemma FT_eq4 : FT_Apeps FT_j0 o FT_t' =_S Id Lim_EoQ.
proof: Proof. apply Trans with (Lim_diese L_A FT_eps). apply (Prf_limit2 L_A). unfold Limit_eq in |- *; intro i. apply Trans with (FT_Apeps FT_j0 o FT_t' o FT_Apeps i). apply Ass1. apply Sym; apply (Eq_cone FT_eps (j:=i) (FT_c3 i)). apply Sym; apply (Prf_limit2 L_A). unfold Limit_eq in |- *; intro i. apply Idl. Qed.
imports: FSC_inc Comma_proj FAFT_SSC2 Th_Adjoint Pres_Limits Pullbacks1