let a, b be Aleph; :: thesis: exp (nextcard a),b = (exp a,b) *` (nextcard a)

now

per cases ( a in b or b c= a ) by CARD_1:14;

suppose a in b ; :: thesis: exp (nextcard a),b = (exp a,b) *` (nextcard a)

then ( nextcard a c= b & b in exp 2,b & a c= b ) by Th23, CARD_1:13, CARD_3:107;
then ( exp (nextcard a),b = exp 2,b & nextcard a in exp 2,b & exp a,b = exp 2,b ) by Th43, ORDINAL1:22;
hence exp (nextcard a),b = (exp a,b) *` (nextcard a) by Th27; :: thesis: verum

end;

suppose b c= a ; :: thesis: exp (nextcard a),b = (exp a,b) *` (nextcard a)

then A1: ( b in nextcard a & cf (nextcard a) = nextcard a ) by Th35, CARD_3:108;
deffunc H₁( Ordinal) -> set = Funcs b,$1;
consider phi being T-Sequence such that
A2: ( dom phi = nextcard a & ( for A being Ordinal st A in nextcard a holds
phi . A = H₁(A) ) ) from ORDINAL2:sch 2();
Funcs b,(nextcard a) c= Union phi

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs b,(nextcard a) or x in Union phi )
assume x in Funcs b,(nextcard a) ; :: thesis: x in Union phi
then consider f being Function such that
A3: ( x = f & dom f = b & rng f c= nextcard a ) by FUNCT_2:def 2;
reconsider f = f as T-Sequence by A3, ORDINAL1:def 7;
reconsider f = f as Ordinal-Sequence by A3, ORDINAL2:def 8;
( sup f in nextcard a & rng f c= sup f ) by A1, A3, Th39, ORDINAL2:67;
then ( f in Funcs b,(sup f) & phi . (sup f) = Funcs b,(sup f) & Union phi = union (rng phi) & phi . (sup f) in rng phi ) by A2, A3, FUNCT_1:def 5, FUNCT_2:def 2;
hence x in Union phi by A3, TARSKI:def 4; :: thesis: verum

end;

then ( card (Funcs b,(nextcard a)) c= card (Union phi) & card (Funcs b,(nextcard a)) = exp (nextcard a),b & card (Union phi) c= Sum (Card phi) ) by CARD_1:27, CARD_2:def 3, CARD_3:54;
then A4: ( exp (nextcard a),b c= Sum (Card phi) & dom (Card phi) = dom phi & dom ((nextcard a) --> (exp a,b)) = nextcard a ) by CARD_3:def 2, FUNCOP_1:19, XBOOLE_1:1;

now

let x be set ; :: thesis: ( x in nextcard a implies (Card phi) . x c= ((nextcard a) --> (exp a,b)) . x )
assume A5: x in nextcard a ; :: thesis: (Card phi) . x c= ((nextcard a) --> (exp a,b)) . x
then reconsider x' = x as Ordinal ;
A6: ( ((nextcard a) --> (exp a,b)) . x = exp a,b & (Card phi) . x = card (phi . x) & phi . x' = Funcs b,x' ) by A2, A5, CARD_3:def 2, FUNCOP_1:13;
A7: ( card (card x) = card x & card x' c= x' & card b = card b ) by CARD_1:24;
card x in nextcard a by A5, CARD_1:24, ORDINAL1:22;
then card x c= a by CARD_3:108;
then Funcs b,(card x) c= Funcs b,a by FUNCT_5:63;
then ( card (Funcs b,(card x)) c= card (Funcs b,a) & card (Funcs b,a) = exp a,b ) by CARD_1:27, CARD_2:def 3;
hence (Card phi) . x c= ((nextcard a) --> (exp a,b)) . x by A6, A7, FUNCT_5:68; :: thesis: verum

end;

then ( Sum (Card phi) c= Sum ((nextcard a) --> (exp a,b)) & Sum ((nextcard a) --> (exp a,b)) = (nextcard a) *` (exp a,b) & (nextcard a) *` (exp a,b) = (exp a,b) *` (nextcard a) ) by A2, A4, CARD_3:43, CARD_3:52;
then A8: exp (nextcard a),b c= (exp a,b) *` (nextcard a) by A4, XBOOLE_1:1;
( a in nextcard a & b c= b & a <> 0 & exp (nextcard a),1 = nextcard a & nextcard a <> 0 & 1 in b ) by Lm1, Th25, CARD_1:32, CARD_2:40;
then ( (exp (nextcard a),b) *` (exp (nextcard a),b) = exp (nextcard a),b & exp a,b c= exp (nextcard a),b & nextcard a c= exp (nextcard a),b ) by CARD_3:138, CARD_4:77;
then (exp a,b) *` (nextcard a) c= exp (nextcard a),b by CARD_3:136;
hence exp (nextcard a),b = (exp a,b) *` (nextcard a) by A8, XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

hence exp (nextcard a),b = (exp a,b) *` (nextcard a) ; :: thesis: verum