let a, b be Aleph; :: thesis:
assume A1: ( cf a c= b & b in a ) ; :: thesis:
( cf a <> 0 & Sum (b -powerfunc_of a) c= exp a,b ) by Th45;
then A2: ( exp (Sum (b -powerfunc_of a)),(cf a) c= exp (exp a,b),(cf a) & b *` (cf a) = b & exp (exp a,b),(cf a) = exp a,(b *` (cf a)) ) by A1, Th27, CARD_2:43, CARD_3:139;
consider phi being Ordinal-Sequence such that
A3: ( dom phi = cf a & rng phi c= a & phi is increasing & a = sup phi & phi is Cardinal-Function & not 0 in rng phi ) by Th41, A1, ORDINAL1:22;
A4: ( exp a,b = card (Funcs b,a) & a = a & 0 = 0 & exp (Sum (b -powerfunc_of a)),(cf a) = card (Funcs (cf a),(Sum (b -powerfunc_of a))) & Sum (b -powerfunc_of a) = card (Union (disjoin (b -powerfunc_of a))) & Sum (b -powerfunc_of a) = card (Sum (b -powerfunc_of a)) & card (cf a) = cf a ) by CARD_1:def 5, CARD_2:def 3;
defpred S₁[ set , set ] means ex g, h being Function st
( g = $1 & h = $2 & dom g = b & rng g c= a & dom h = cf a & ( for y being set st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) ) );
A5: for x being set st x in Funcs b,a holds
ex x1 being set st S₁[x,x1]

proof

let x be set ; :: thesis:
assume x in Funcs b,a ; :: thesis:
then consider g being Function such that
A6: ( x = g & dom g = b & rng g c= a ) by FUNCT_2:def 2;
defpred S₂[ set , set ] means ex fx being Function st
( $2 = [fx,(phi . $1)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . $1 implies fx . z = g . z ) & ( not g . z in phi . $1 implies fx . z = 0 ) ) ) );
A7: for y being set st y in cf a holds
ex x2 being set st S₂[y,x2]

proof

let y be set ; :: thesis:
assume y in cf a ; :: thesis:
deffunc H₁( set ) -> set = g . $1;
deffunc H₂( set ) -> Element of NAT = 0 ;
defpred S₃[ set ] means g . $1 in phi . y;
consider fx being Function such that
A8: ( dom fx = b & ( for z being set st z in b holds
( ( S₃[z] implies fx . z = H₁(z) ) & ( not S₃[z] implies fx . z = H₂(z) ) ) ) ) from PARTFUN1:sch 1();
take [fx,(phi . y)] ; :: thesis:
take fx ; :: thesis:
thus ( [fx,(phi . y)] = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) by A8; :: thesis:

end;

consider h being Function such that
A9: ( dom h = cf a & ( for y being set st y in cf a holds
S₂[y,h . y] ) ) from CLASSES1:sch 1(A7);
take h ; :: thesis:
take g ; :: thesis:
take h ; :: thesis:
thus ( g = x & h = h & dom g = b & rng g c= a & dom h = cf a & ( for y being set st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) ) ) by A6, A9; :: thesis:

end;

consider f being Function such that
A10: ( dom f = Funcs b,a & ( for x being set st x in Funcs b,a holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A5);
A11: f is one-to-one

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis:
let y be set ; :: thesis:
assume A12: ( x in dom f & y in dom f & f . x = f . y ) ; :: thesis:
then consider g1, h1 being Function such that
A13: ( g1 = x & h1 = f . x & dom g1 = b & rng g1 c= a & dom h1 = cf a & ( for x1 being set st x1 in cf a holds
ex fx being Function st
( h1 . x1 = [fx,(phi . x1)] & dom fx = b & ( for z being set st z in b holds
( ( g1 . z in phi . x1 implies fx . z = g1 . z ) & ( not g1 . z in phi . x1 implies fx . z = 0 ) ) ) ) ) ) by A10;
consider g2, h2 being Function such that
A14: ( g2 = y & h2 = f . y & dom g2 = b & rng g2 c= a & dom h2 = cf a & ( for x2 being set st x2 in cf a holds
ex fx being Function st
( h2 . x2 = [fx,(phi . x2)] & dom fx = b & ( for z being set st z in b holds
( ( g2 . z in phi . x2 implies fx . z = g2 . z ) & ( not g2 . z in phi . x2 implies fx . z = 0 ) ) ) ) ) ) by A10, A12;

now

let x1 be set ; :: thesis:
assume x1 in b ; :: thesis:
then reconsider X = x1 as Element of b ;
( g1 . X in rng g1 & g2 . X in rng g2 ) by A13, A14, FUNCT_1:def 5;
then reconsider A1 = g1 . x1, A2 = g2 . x1 as Element of a by A13, A14;
set A = A1 \/ A2;
( ( A1 \/ A2 = A1 or A1 \/ A2 = A2 ) & a is limit_ordinal ) by ORDINAL3:15;
then ( succ (A1 \/ A2) in a & sup phi = sup (rng phi) ) by ORDINAL1:41;
then consider B being Ordinal such that
A15: ( B in rng phi & succ (A1 \/ A2) c= B ) by A3, ORDINAL2:29;
consider x2 being set such that
A16: ( x2 in dom phi & B = phi . x2 ) by A15, FUNCT_1:def 5;
consider f1 being Function such that
A17: ( h1 . x2 = [f1,(phi . x2)] & dom f1 = b & ( for z being set st z in b holds
( ( g1 . z in phi . x2 implies f1 . z = g1 . z ) & ( not g1 . z in phi . x2 implies f1 . z = 0 ) ) ) ) by A3, A13, A16;
consider f2 being Function such that
A18: ( h2 . x2 = [f2,(phi . x2)] & dom f2 = b & ( for z being set st z in b holds
( ( g2 . z in phi . x2 implies f2 . z = g2 . z ) & ( not g2 . z in phi . x2 implies f2 . z = 0 ) ) ) ) by A3, A14, A16;
( A1 c= A1 \/ A2 & A2 c= A1 \/ A2 & A1 \/ A2 in succ (A1 \/ A2) ) by ORDINAL1:10, XBOOLE_1:7;
then ( A1 in B & A2 in B & f1 = f2 ) by A12, A13, A14, A15, A17, A18, ORDINAL1:22, ZFMISC_1:33;
then ( f1 . X = g1 . x1 & f1 . X = g2 . x1 ) by A16, A17, A18;
hence g1 . x1 = g2 . x1 ; :: thesis:

end;

hence x = y by A13, A14, FUNCT_1:9; :: thesis:

end;

deffunc H₁( set ) -> set = Funcs b,$1;
consider F being Function such that
A19: ( dom F = dom (b -powerfunc_of a) & ( for x being set st x in dom (b -powerfunc_of a) holds
F . x = H₁(x) ) ) from FUNCT_1:sch 3();
rng f c= Funcs (cf a),(Union (disjoin F))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being set such that
A20: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
consider g, h being Function such that
A21: ( g = x & h = f . x & dom g = b & rng g c= a & dom h = cf a & ( for y being set st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . y implies fx . z = g . z ) & ( not g . z in phi . y implies fx . z = 0 ) ) ) ) ) ) by A10, A20;
rng h c= Union (disjoin F)

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis:
assume x1 in rng h ; :: thesis:
then consider x2 being set such that
A22: ( x2 in dom h & x1 = h . x2 ) by FUNCT_1:def 5;
consider fx being Function such that
A23: ( x1 = [fx,(phi . x2)] & dom fx = b & ( for z being set st z in b holds
( ( g . z in phi . x2 implies fx . z = g . z ) & ( not g . z in phi . x2 implies fx . z = 0 ) ) ) ) by A21, A22;
rng fx c= phi . x2

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in rng fx ; :: thesis:
then consider z' being set such that
A24: ( z' in dom fx & z = fx . z' ) by FUNCT_1:def 5;
reconsider x2 = x2 as Ordinal by A21, A22;
reconsider A = phi . x2 as Ordinal ;
( ( g . z' in phi . x2 or not g . z' in phi . x2 ) & A <> 0 ) by A3, A21, A22, FUNCT_1:def 5;
then ( ( ( z = g . z' & g . z' in phi . x2 ) or z = 0 ) & 0 in A ) by A23, A24, ORDINAL3:10;
hence z in phi . x2 ; :: thesis:

end;

then A25: fx in Funcs b,(phi . x2) by A23, FUNCT_2:def 2;
phi . x2 in rng phi by A3, A21, A22, FUNCT_1:def 5;
then ( phi . x2 is Cardinal & phi . x2 in a ) by A3, A21, A22, CARD_3:def 1;
then A26: phi . x2 in dom (b -powerfunc_of a) by Def3;
then ( F . (phi . x2) = Funcs b,(phi . x2) & [fx,(phi . x2)] `1 = fx & [fx,(phi . x2)] `2 = phi . x2 ) by A19, MCART_1:7;
hence x1 in Union (disjoin F) by A19, A23, A25, A26, CARD_3:33; :: thesis:

end;

hence y in Funcs (cf a),(Union (disjoin F)) by A20, A21, FUNCT_2:def 2; :: thesis:

end;

then A27: exp a,b c= card (Funcs (cf a),(Union (disjoin F))) by A4, A10, A11, CARD_1:26;
( card (card (Union (disjoin F))) = card (Union (disjoin F)) & card (cf a) = cf a ) by CARD_1:def 5;
then A28: card (Funcs (cf a),(Union (disjoin F))) = card (Funcs (cf a),(card (Union (disjoin F)))) by FUNCT_5:68
.= exp (card (Union (disjoin F))),(cf a) by CARD_2:def 3 ;
A29: ( dom (Card (disjoin F)) = dom (disjoin F) & dom (disjoin F) = dom F & dom (Card F) = dom F ) by CARD_3:def 2, CARD_3:def 3;

now

let x be set ; :: thesis:
assume x in dom F ; :: thesis:
then ( (Card F) . x = card (F . x) & (Card (disjoin F)) . x = card ((disjoin F) . x) & (disjoin F) . x = [:(F . x),{x}:] ) by A29, CARD_3:def 2, CARD_3:def 3;
hence (Card (disjoin F)) . x = (Card F) . x by CARD_2:13; :: thesis:

end;

then A30: Card F = Card (disjoin F) by A29, FUNCT_1:9;

now

let x be set ; :: thesis:
assume A31: x in dom F ; :: thesis:
then A32: ( (Card F) . x = card (F . x) & F . x = Funcs b,x ) by A19, CARD_3:def 2;
reconsider M = x as Cardinal by A19, A31, Def3;
M in a by A19, A31, Def3;
then (b -powerfunc_of a) . M = exp M,b by Def3;
hence (Card F) . x = (b -powerfunc_of a) . x by A32, CARD_2:def 3; :: thesis:

end;

then Card F = b -powerfunc_of a by A19, A29, FUNCT_1:9;
then ( cf a <> 0 & card (Union (disjoin F)) c= Sum (b -powerfunc_of a) ) by A30, CARD_3:54;
then exp (card (Union (disjoin F))),(cf a) c= exp (Sum (b -powerfunc_of a)),(cf a) by CARD_3:139;
then exp a,b c= exp (Sum (b -powerfunc_of a)),(cf a) by A27, A28, XBOOLE_1:1;
hence exp a,b = exp (Sum (b -powerfunc_of a)),(cf a) by A2, XBOOLE_0:def 10; :: thesis: