proposition: Lemma PhiCone_1_fun_cone_law : Cone_law PhiCone_1_fun_tau.
proof: Proof. unfold Cone_law, PhiCone_1_fun_tau in |- *; simpl in |- *. intros i j g. apply Trans with (f o Limiting_cone l i o FMor F g). apply Comp_l; apply (EqC (Limiting_cone l) g). apply Ass. Qed.
imports: SET Limit Map0_dup1