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

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in Funcs b,a ; :: thesis:
then consider f being Function such that
A3: ( x = f & dom f = b & rng f c= 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 a & rng f c= sup f ) by A1, A3, Th39, ORDINAL2:67;
then ( x in Funcs b,(sup f) & L . (sup f) = Funcs b,(sup f) & L . (sup f) in rng L ) by A2, A3, FUNCT_1:def 5, FUNCT_2:def 2;
hence x in Union L by TARSKI:def 4; :: thesis:

end;

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

let x be set ; :: thesis:
assume A7: x in a ; :: thesis:
then reconsider x' = x as Ordinal ;
set m = card x';
( b,b are_equipotent & x', card x' are_equipotent ) by CARD_1:def 5;
then ( L . x = Funcs b,x' & (Card L) . x = card (L . x) & card (Funcs b,x') = card (Funcs b,(card x')) & card x' c= x' ) by A2, A7, CARD_1:24, CARD_3:def 2, FUNCT_5:67;
then A8: ( (Card L) . x = exp (card x'),b & card x' in a ) by A7, CARD_2:def 3, ORDINAL1:22;
then card x' in dom (b -powerfunc_of a) by Def3;
then ( (b -powerfunc_of a) . (card x) = exp (card x),b & (b -powerfunc_of a) . (card x) in rng (b -powerfunc_of a) ) by A8, Def3, FUNCT_1:def 5;
then ( card (exp (card x),b) c= card (Union (b -powerfunc_of a)) & card (Union (b -powerfunc_of a)) c= Sum (b -powerfunc_of a) ) by CARD_1:27, CARD_3:55, ZFMISC_1:92;
then ( card (exp (card x),b) c= Sum (b -powerfunc_of a) & card (exp (card x),b) = exp (card x),b ) by CARD_1:def 5, XBOOLE_1:1;
hence (Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x by A7, A8, FUNCOP_1:13; :: thesis:

end;

then ( Sum (Card L) c= Sum (a --> (Sum (b -powerfunc_of a))) & Sum (a --> (Sum (b -powerfunc_of a))) = a *` (Sum (b -powerfunc_of a)) ) by A2, A6, CARD_3:43, CARD_3:52;
then A9: exp a,b c= a *` (Sum (b -powerfunc_of a)) by A4, XBOOLE_1:1;
a c= Sum (b -powerfunc_of a)

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A10: x in a ; :: thesis:
then reconsider x' = x as Ordinal ;
set m = card x';
card x' in a by A10, CARD_1:24, ORDINAL1:22;
then ( nextcard (card x') c= a & nextcard (card x') <> a ) by A1, CARD_1:def 7, CARD_3:107;
then A11: nextcard (card x') in a by CARD_1:13;
then nextcard (card x') in dom (b -powerfunc_of a) by Def3;
then ( (b -powerfunc_of a) . (nextcard (card x')) in rng (b -powerfunc_of a) & (b -powerfunc_of a) . (nextcard (card x')) = exp (nextcard (card x')),b ) by A11, Def3, FUNCT_1:def 5;
then exp (nextcard (card x')),b c= Union (b -powerfunc_of a) by ZFMISC_1:92;
then ( card (exp (nextcard (card x')),b) = exp (nextcard (card x')),b & card (exp (nextcard (card x')),b) c= card (Union (b -powerfunc_of a)) & card (Union (b -powerfunc_of a)) c= Sum (b -powerfunc_of a) ) by CARD_1:27, CARD_1:def 5, CARD_3:55;
then ( exp (nextcard (card x')),b c= Sum (b -powerfunc_of a) & nextcard (card x') c= exp (nextcard (card x')),b ) by Th31, XBOOLE_1:1;
then A12: nextcard (card x) c= Sum (b -powerfunc_of a) by XBOOLE_1:1;
card x = card (card x) ;
then ( x' in nextcard x' & nextcard (card x) = nextcard x ) by CARD_1:36, CARD_3:105;
hence x in Sum (b -powerfunc_of a) by A12; :: thesis:

end;

then a *` (Sum (b -powerfunc_of a)) = Sum (b -powerfunc_of a) by Th27;
hence exp a,b = Sum (b -powerfunc_of a) by A5, A9, XBOOLE_0:def 10; :: thesis: