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

now :: thesis: exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a)

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

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

then a c= b by CARD_1:3;
then A2: exp (a,b) = exp (2,b) by Th30;
nextcard a c= b by A1, CARD_3:90;
then ( exp ((nextcard a),b) = exp (2,b) & nextcard a in exp (2,b) ) by Th14, Th30, ORDINAL1:12;
hence exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a) by A2, Th17; :: 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 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 Th22;
A6: b in nextcard a by A3, CARD_3:91;
Funcs (b,(nextcard a)) c= Union phi

proof

let x be object ; :: 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 Sequence by A8, ORDINAL1:def 7;
reconsider f = f as Ordinal-Sequence by A9, ORDINAL2:def 4;
sup f in nextcard a by A6, A5, A8, A9, Th26;
then A10: phi . (sup f) in rng phi by A4, FUNCT_1:def 3;
rng f c= sup f by ORDINAL2:49;
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, Th26;
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:11;
( card (Funcs (b,(nextcard a))) = exp ((nextcard a),b) & card (Union phi) c= Sum (Card phi) ) by CARD_2:def 3, CARD_3:39;
then A13: exp ((nextcard a),b) c= Sum (Card phi) by A12;
a in nextcard a by CARD_1:18;
then A14: ( (exp ((nextcard a),b)) *` (exp ((nextcard a),b)) = exp ((nextcard a),b) & exp (a,b) c= exp ((nextcard a),b) ) by CARD_2:92, CARD_4:15;
( exp ((nextcard a),1) = nextcard a & 1 in b ) by Lm1, Th15, CARD_2:27;
then nextcard a c= exp ((nextcard a),b) by CARD_2:92;
then A15: (exp (a,b)) *` (nextcard a) c= exp ((nextcard a),b) by A14, CARD_2:90;

A16: now :: thesis: for x being object st x in nextcard a holds
(Card phi) . x c= ((nextcard a) --> (exp (a,b))) . x

let x be object ; :: thesis: ( x in nextcard a implies (Card phi) . x c= ((nextcard a) --> (exp (a,b))) . x )
reconsider xx = x as set by TARSKI:1;
A17: ( card (card xx) = card xx & 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 xx in nextcard a by A18, CARD_1:8, ORDINAL1:12;
then card xx c= a by CARD_3:91;
then Funcs (b,(card xx)) c= Funcs (b,a) by FUNCT_5:56;
then A20: card (Funcs (b,(card xx))) c= card (Funcs (b,a)) by CARD_1:11;
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:7;
hence (Card phi) . x c= ((nextcard a) --> (exp (a,b))) . x by A19, A17, A20, A21, FUNCT_5:61; :: thesis: verum

end;

( dom (Card phi) = dom phi & dom ((nextcard a) --> (exp (a,b))) = nextcard a ) by CARD_3:def 2;
then A22: Sum (Card phi) c= Sum ((nextcard a) --> (exp (a,b))) by A4, A16, CARD_3:30;
Sum ((nextcard a) --> (exp (a,b))) = (nextcard a) *` (exp (a,b)) by CARD_2:65;
then exp ((nextcard a),b) c= (exp (a,b)) *` (nextcard a) by A13, A22;
hence exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a) by A15; :: thesis: verum

end;

end;

end;

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