proposition: Lemma infinite_prod_pG b: \1o <=o b -> cprodb omega1 (fun z => (\aleph z) ^c (\aleph b)) = (\aleph omega1) ^c (\aleph b).
proof: Proof. move => b1. have cp1: aleph1 <=c \aleph b by apply:aleph_le_lec b1. have ie := CIS_aleph (proj32 b1). move: (f_equal (fun z => z ^c \aleph b) infinite_prod_pF). aw;rewrite cpow_prod - cpow_pow cprodC (cprod_inf cp1 ie (aleph_nz OS1)) => <-. by aw;apply: cprodb_exten => x xe; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)