proposition: Lemma infinite_prod3_bis X m (Y:= Lg (domain X) (fun z => \aleph (Vg X z))): infinite_c m -> ofg_Mlt_lto X -> domain X = m -> (cprod Y) = (\csup (range Y)) ^c m.
proof: Proof. move => im pa pb. have idx:= (cardinal_indecomposable im). have [y oy xv]:=(indecomp_prop3 idx). case: (ozero_dichot oy) => ynz. by move: im; rewrite xv ynz oopow0=> /(finite_not_infinite finite_1). rewrite xv in pb. by rewrite (infinite_prod3 ynz pa pb) xv cpowcr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)