proposition: Lemma infinite_prod4 X a m (Y:= Lg (domain X) (fun z => \aleph (Vg X z) ^c m)): limit_ordinal a -> \cf a <=c m -> domain X = \cf a -> ofg_Mlt_lto X -> a = \osup (range X) -> cprod Y = \aleph a ^c m.
proof: Proof. move => oa ca cdx ofx av. have icc:=(cofinality_infinite_limit oa). have im:= cle_inf_inf icc ca. move:(cofinality_limit3 oa); rewrite - cdx => lc. move: (infinite_prod3_bis icc ofx cdx). move: (increasing_sup_limit4 ofx lc); rewrite -av; move => [pa _ ->] => pd. move: (f_equal (fun z => z ^c m) pd). rewrite - cpow_pow cpow_prod cprodC (cprod_inf ca im (infinite_nz icc)). by move => <-; aw; rewrite /Y cdx; apply: cprodb_exten => x xd; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)