let a, b be Aleph; :: thesis: ( a is limit_cardinal & b in cf a implies exp (a,b) = Sum (b -powerfunc_of a) )
assume that
A1: a is limit_cardinal and
A2: b in cf a ; :: thesis: exp (a,b) = Sum (b -powerfunc_of a)
deffunc H₁( Ordinal) -> set = Funcs (b,$1);
consider L being Sequence such that
A3: ( dom L = a & ( for A being Ordinal st A in a holds
L . A = H₁(A) ) ) from ORDINAL2:sch 2();

A4: now :: thesis: for x being object st x in a holds
(Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x

let x be object ; :: thesis: ( x in a implies (Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x )
A5: card (Union (b -powerfunc_of a)) c= Sum (b -powerfunc_of a) by CARD_3:40;
assume A6: x in a ; :: thesis: (Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x
then reconsider x9 = x as Ordinal ;
set m = card x9;
A7: card x9 in a by A6, CARD_1:8, ORDINAL1:12;
then card x9 in dom (b -powerfunc_of a) by Def2;
then A8: (b -powerfunc_of a) . (card x9) in rng (b -powerfunc_of a) by FUNCT_1:def 3;
x9, card x9 are_equipotent by CARD_1:def 2;
then A9: card (Funcs (b,x9)) = card (Funcs (b,(card x9))) by FUNCT_5:60;
( L . x = Funcs (b,x9) & (Card L) . x = card (L . x) ) by A3, A6, CARD_3:def 2;
then A10: (Card L) . x = exp ((card x9),b) by A9, CARD_2:def 3;
(b -powerfunc_of a) . (card x9) = exp ((card x9),b) by A7, Def2;
then card (exp ((card x9),b)) c= card (Union (b -powerfunc_of a)) by A8, CARD_1:11, ZFMISC_1:74;
then A11: card (exp ((card x9),b)) c= Sum (b -powerfunc_of a) by A5;
thus (Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x by A6, A10, A11, FUNCOP_1:7; :: thesis: verum

end;

( dom (a --> (Sum (b -powerfunc_of a))) = a & dom (Card L) = dom L ) by CARD_3:def 2;
then A12: Sum (Card L) c= Sum (a --> (Sum (b -powerfunc_of a))) by A3, A4, CARD_3:30;
a c= Sum (b -powerfunc_of a)

proof

let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in a or x in Sum (b -powerfunc_of a) )
reconsider xx = x as set ;
assume A13: x in a ; :: thesis: x in Sum (b -powerfunc_of a)
reconsider x9 = x as Ordinal ;
set m = card x9;
card x9 in a by A13, CARD_1:8, ORDINAL1:12;
then A14: nextcard (card x9) c= a by CARD_3:90;
nextcard (card x9) <> a by A1;
then A15: nextcard (card x9) in a by A14, CARD_1:3;
then nextcard (card x9) in dom (b -powerfunc_of a) by Def2;
then A16: (b -powerfunc_of a) . (nextcard (card x9)) in rng (b -powerfunc_of a) by FUNCT_1:def 3;
(b -powerfunc_of a) . (nextcard (card x9)) = exp ((nextcard (card x9)),b) by A15, Def2;
then A17: card (exp ((nextcard (card x9)),b)) c= card (Union (b -powerfunc_of a)) by A16, CARD_1:11, ZFMISC_1:74;
A18: nextcard (card x9) c= exp ((nextcard (card x9)),b) by Th19;
card xx = card (card xx) ;
then A19: ( x9 in nextcard x9 & nextcard (card xx) = nextcard xx ) by CARD_1:18, CARD_3:88;
( card (exp ((nextcard (card x9)),b)) = exp ((nextcard (card x9)),b) & card (Union (b -powerfunc_of a)) c= Sum (b -powerfunc_of a) ) by CARD_3:40;
then exp ((nextcard (card x9)),b) c= Sum (b -powerfunc_of a) by A17;
then nextcard (card xx) c= Sum (b -powerfunc_of a) by A18;
hence x in Sum (b -powerfunc_of a) by A19; :: thesis: verum

end;

then A20: a *` (Sum (b -powerfunc_of a)) = Sum (b -powerfunc_of a) by Th17;
Funcs (b,a) c= Union L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs (b,a) or x in Union L )
assume x in Funcs (b,a) ; :: thesis: x in Union L
then consider f being Function such that
A21: x = f and
A22: dom f = b and
A23: rng f c= a by FUNCT_2:def 2;
reconsider f = f as Sequence by A22, ORDINAL1:def 7;
reconsider f = f as Ordinal-Sequence by A23, ORDINAL2:def 4;
rng f c= sup f by ORDINAL2:49;
then A24: x in Funcs (b,(sup f)) by A21, A22, FUNCT_2:def 2;
sup f in a by A2, A22, A23, Th26;
then A25: L . (sup f) in rng L by A3, FUNCT_1:def 3;
L . (sup f) = Funcs (b,(sup f)) by A2, A3, A22, A23, Th26;
hence x in Union L by A24, A25, TARSKI:def 4; :: thesis: verum

end;

then A26: card (Funcs (b,a)) c= card (Union L) by CARD_1:11;
card (Union L) c= Sum (Card L) by CARD_3:39;
then card (Funcs (b,a)) c= Sum (Card L) by A26;
then A27: exp (a,b) c= Sum (Card L) by CARD_2:def 3;
A28: Sum (b -powerfunc_of a) c= exp (a,b) by Th32;
Sum (a --> (Sum (b -powerfunc_of a))) = a *` (Sum (b -powerfunc_of a)) by CARD_2:65;
then exp (a,b) c= a *` (Sum (b -powerfunc_of a)) by A27, A12;
hence exp (a,b) = Sum (b -powerfunc_of a) by A28, A20; :: thesis: verum