proposition: Lemma infinite_prod44 X a b (Y:= Lg (domain X) (fun z => \aleph (Vg X z) ^c \aleph b)): limit_ordinal a -> \cf a <=o b -> domain X = \omega (\cf a) -> ofg_Mlt_lto X -> a = \osup (range X) -> cprod Y = \aleph a ^c (\aleph b).
proof: Proof. move => oa ca cdx ofx av. have oc:=(OS_cofinality (proj31 oa)). have icc:=(CIS_aleph oc). have lc:= (infinite_card_limit2 icc). move: (infinite_prod3_bis icc ofx cdx). rewrite - cdx in lc. move:(increasing_sup_limit4 ofx lc); rewrite - av; move => [pa _ ->] => pd. move: (f_equal (fun z => z ^c \aleph b) pd). rewrite - cpow_pow cpow_prod cprodC. rewrite (cprod_inf (aleph_le_lec ca) (CIS_aleph (proj32 ca))(infinite_nz icc)). by move => <-; aw; rewrite /Y cdx; apply: cprodb_exten => x xd; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)