proposition: Theorem cprod_one_unit f j: sub j (domain f) -> (forall i, inc i ((domain f) -s j) -> (Vg f i) = \1c) -> cprod f = cprodb j (Vg f).
proof: Proof. move=> jdf alo; apply /card_eqP; exists (pr_j f j). by apply: (prj_fb jdf) => i /alo ->; exists emptyset. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)