proposition: Lemma FS_diese_map_law : Map_law FS_diese_mor.
proof: Proof. unfold Map_law in |- *; intros x y H. unfold FS_diese_mor in |- *. apply (Ldiese_map l). simpl in |- *; unfold Equal_NT in |- *; intro i; simpl in |- *. unfold FS_cone_tau in |- *. apply Pres1; assumption. Qed.
imports: HomFunctor Pres_Limits