proposition: Lemma FS_limit2 : Limit_law2 FS_lcone FS_diese.
proof: Proof. unfold Limit_law2 in |- *; intros X tau f. unfold Limit_eq, FS_diese in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. unfold FunSET_mor1, FS_diese_mor in |- *. intros H x. unfold FunSET_ob in |- *. apply (Prf_limit2 l). unfold Limit_eq in |- *; simpl in |- *. intro i; apply (H i x). Qed.
imports: HomFunctor Pres_Limits