proposition: Lemma Tc_UA_law2 : Limit_law2 Tc_limconeF Tc_diese.
proof: Proof. unfold Limit_law2, Limit_eq in |- *; intros axf t g. intro H; unfold Tc_diese in |- *; simpl in |- *; unfold Equal_com_arrow in |- *; simpl in |- *. apply (Prf_limit2 l_F'). exact H. Qed.
imports: Pres_Limits Comma_proj