proposition: Lemma FT_h_diese_unique : FT_h' =_S FT_h_diese.
proof: Proof. unfold FT_h_diese in |- *. apply Trans with (Id Lim_EoQ o FT_h'). apply Idl1. apply Trans with (FT_Apeps FT_j0 o FT_t' o FT_h'). apply Trans with ((FT_Apeps FT_j0 o FT_t') o FT_h'). apply Comp_r. apply Sym; apply FT_eq4. apply Ass1. apply Sym; apply FT_diag4. Qed.
imports: FSC_inc Comma_proj FAFT_SSC2 Th_Adjoint Pres_Limits Pullbacks1