proposition: Lemma FS_limit1 : Limit_law1 FS_lcone FS_diese.
proof: Proof. unfold Limit_law1, Limit_eq in |- *; simpl in |- *. intros X tau i. unfold Ext in |- *; intro x. unfold Comp_cone in |- *; simpl in |- *. unfold FunSET_mor1, FS_diese_mor in |- *; simpl in |- *. apply (Prf_limit1 l (FS_cone tau x) i). Qed.
imports: HomFunctor Pres_Limits