proposition: Lemma Thl_limit1 : Limit_law1 Thl_mu Thl_diese.
proof: Proof. unfold Limit_law1, Limit_eq in |- *; intros c tau; simpl in |- *; intro i. apply Trans with ((Thl_diese tau o Thl_e) o Proj1 Thl_l_Fi i). apply Trans with (Thl_diese tau o Thl_e o Proj1 Thl_l_Fi i). apply Refl. apply Ass. apply Trans with (Pd1_diese Thl_l_Fi (c:=c) (fun i : J => tau i) o Proj1 Thl_l_Fi i). apply Comp_r. apply Sym. apply (Prf_E1_law2 Thl_l_fg (Prf_law1_fg (Thl_diag4 tau))). apply Sym. apply (Thl_diag3 tau i). Qed.
imports: Equalizers1 Products1