proposition: Lemma FunDiscr_comp_law : Fcomp_law FunDiscr_map.
proof: Proof. unfold Fcomp_law in |- *; intros i j k f. elim f; simpl in |- *. intros i' g; elim g; simpl in |- *. intro i''; unfold Comp in |- *; apply (Prf_idr (c:=C)). Qed.
imports: Limit Discr Products