proposition: Lemma infinite_increasing_power2 X b: ofg_Mlt_lto X -> domain X = \omega b -> ordinalp b -> cprod (Lg (domain X) (fun z => \aleph (Vg X z))) = \aleph (\osup (range X)) ^c \aleph b.
proof: Proof. move=> p1 p3 p4. have lb: limit_ordinal (domain X) by rewrite p3; apply: aleph_limit. move: ( ofg_Mlt_lto_p3 p1 lb) => p2. by apply: infinite_increasing_power1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)