proposition: Lemma finite_family_product a f: fgraph f -> finite_set (domain f) -> infinite_c a -> (forall i, inc i (domain f) -> (Vg f i) <=c a) -> card_nz_fam f -> (exists2 j, inc j (domain f) & (Vg f j) = a) -> cprod f = a.
proof: Proof. move=> fgf fsd ifa alea alnz [j0 j0d vj0]. set (g:= cst_graph (domain f) a). have fgg: fgraph g by rewrite /g /cst_graph; fprops. have df: domain f = domain g by rewrite /g/cst_graph Lgd. have le1:forall x, inc x (domain f) -> (Vg f x) <=c (Vg g x). by move=> t tdf; rewrite /g/cst_graph LgV//; apply: alea. move: (cprod_increasing df le1); rewrite [cprod g] cprod_of_same. set (n:= cardinal (domain f)). have nN: natp n by fprops. have nz: n <> \0c by apply: card_nonempty1; exists j0 =>//. rewrite - cpowcr (cpow_inf ifa nN nz)=> le0. set (j:= singleton j0). have alc: (forall x, inc x (domain f) -> cardinalp (Vg f x)). by move=> x xdf; move: (alea _ xdf) => [h _]. move: (alc _ j0d); rewrite vj0 => ca. have sjd: (sub j (domain f)) by move=> t /set1_P => ->. move: (cprod_increasing1 alnz sjd). by rewrite /j cprod_trivial4 // vj0 (card_card ca) => /(cleA le0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)