proposition: Lemma Thl_limit2 : Limit_law2 Thl_mu Thl_diese.
proof: Proof. unfold Limit_law2, Limit_eq in |- *; intros c tau t H. unfold Thl_diese in |- *; apply (Prf_E1_law3 (l:=Thl_l_fg)). apply Sym. unfold Thl_h in |- *. apply (Prf_pd1_law2 (l:=Thl_l_Fi)); unfold Product_eq in |- *; intro i. apply Trans with (t o Thl_e o Proj1 Thl_l_Fi i). apply Sym. exact (H i). apply Ass. Qed.
imports: Equalizers1 Products1