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 A1: a in b ; :: thesis: exp (nextcard a),b = (exp a,b) *` (nextcard a)

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

end;

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

deffunc H₁( Ordinal) -> set = Funcs b,$1;
consider phi being T-Sequence such that
A4: ( dom phi = nextcard a & ( for A being Ordinal st A in nextcard a holds
phi . A = H₁(A) ) ) from ORDINAL2:sch 2();
A5: cf (nextcard a) = nextcard a by Th35;
A6: b in nextcard a by A3, CARD_3:108;
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
A7: x = f and
A8: dom f = b and
A9: rng f c= nextcard a by FUNCT_2:def 2;
reconsider f = f as T-Sequence by A8, ORDINAL1:def 7;
reconsider f = f as Ordinal-Sequence by A9, ORDINAL2:def 8;
sup f in nextcard a by A6, A5, A8, A9, Th39;
then A10: phi . (sup f) in rng phi by A4, FUNCT_1:def 5;
rng f c= sup f by ORDINAL2:67;
then A11: f in Funcs b,(sup f) by A8, FUNCT_2:def 2;
phi . (sup f) = Funcs b,(sup f) by A6, A5, A4, A8, A9, Th39;
hence x in Union phi by A7, A11, A10, TARSKI:def 4; :: thesis: verum

end;

then A12: card (Funcs b,(nextcard a)) c= card (Union phi) by CARD_1:27;
( card (Funcs b,(nextcard a)) = exp (nextcard a),b & card (Union phi) c= Sum (Card phi) ) by CARD_2:def 3, CARD_3:54;
then A13: exp (nextcard a),b c= Sum (Card phi) by A12, XBOOLE_1:1;
a in nextcard a by CARD_1:32;
then A14: ( (exp (nextcard a),b) *` (exp (nextcard a),b) = exp (nextcard a),b & exp a,b c= exp (nextcard a),b ) by CARD_3:138, CARD_4:77;
( exp (nextcard a),1 = nextcard a & 1 in b ) by Lm1, Th25, CARD_2:40;
then nextcard a c= exp (nextcard a),b by CARD_3:138;
then A15: (exp a,b) *` (nextcard a) c= exp (nextcard a),b by A14, CARD_3:136;

A16: now

let x be set ; :: thesis: ( x in nextcard a implies (Card phi) . x c= ((nextcard a) --> (exp a,b)) . x )
A17: ( card (card x) = card x & card b = card b ) ;
assume A18: x in nextcard a ; :: thesis: (Card phi) . x c= ((nextcard a) --> (exp a,b)) . x
then reconsider x9 = x as Ordinal ;
A19: phi . x9 = Funcs b,x9 by A4, A18;
card x in nextcard a by A18, 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 A20: card (Funcs b,(card x)) c= card (Funcs b,a) by CARD_1:27;
A21: card (Funcs b,a) = exp a,b by CARD_2:def 3;
( ((nextcard a) --> (exp a,b)) . x = exp a,b & (Card phi) . x = card (phi . x) ) by A4, A18, CARD_3:def 2, FUNCOP_1:13;
hence (Card phi) . x c= ((nextcard a) --> (exp a,b)) . x by A19, A17, A20, A21, FUNCT_5:68; :: thesis: verum

end;

( dom (Card phi) = dom phi & dom ((nextcard a) --> (exp a,b)) = nextcard a ) by CARD_3:def 2, FUNCOP_1:19;
then A22: Sum (Card phi) c= Sum ((nextcard a) --> (exp a,b)) by A4, A16, CARD_3:43;
Sum ((nextcard a) --> (exp a,b)) = (nextcard a) *` (exp a,b) by CARD_3:52;
then exp (nextcard a),b c= (exp a,b) *` (nextcard a) by A13, A22, XBOOLE_1:1;
hence exp (nextcard a),b = (exp a,b) *` (nextcard a) by A15, XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

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