let a, b be Aleph; :: thesis: ( cf a c= b & b in a implies exp a,b = exp (Sum (b -powerfunc_of a)),(cf a) )
assume that
A1: cf a c= b and
A2: b in a ; :: thesis: exp a,b = exp (Sum (b -powerfunc_of a)),(cf a)
consider phi being Ordinal-Sequence such that
A3: dom phi = cf a and
A4: rng phi c= a and
phi is increasing and
A5: a = sup phi and
A6: phi is Cardinal-Function and
A7: not 0 in rng phi by A1, A2, Th41, ORDINAL1:22;
defpred S1[ 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 ) ) ) ) ) );
A8: for x being set st x in Funcs b,a holds
ex x1 being set st S1[x,x1]
proof
let x be set ; :: thesis: ( x in Funcs b,a implies ex x1 being set st S1[x,x1] )
assume x in Funcs b,a ; :: thesis: ex x1 being set st S1[x,x1]
then consider g being Function such that
A9: ( x = g & dom g = b & rng g c= a ) by FUNCT_2:def 2;
defpred S2[ 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 ) ) ) );
A10: for y being set st y in cf a holds
ex x2 being set st S2[y,x2]
proof
deffunc H1( set ) -> Element of NAT = 0 ;
deffunc H2( set ) -> set = g . $1;
let y be set ; :: thesis: ( y in cf a implies ex x2 being set st S2[y,x2] )
assume y in cf a ; :: thesis: ex x2 being set st S2[y,x2]
defpred S3[ set ] means g . $1 in phi . y;
consider fx being Function such that
A11: ( dom fx = b & ( for z being set st z in b holds
( ( S3[z] implies fx . z = H2(z) ) & ( not S3[z] implies fx . z = H1(z) ) ) ) ) from PARTFUN1:sch 1();
 take [fx,(phi . y)] ; :: thesis: S2[y,[fx,(phi . y)]]
take fx ; :: thesis: ( [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 ) ) ) )
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 A11; :: thesis: verum
end;
consider h being Function such that
A12: ( dom h = cf a & ( for y being set st y in cf a holds
S2[y,h . y] ) ) from CLASSES1:sch 1(A10);
 take h ; :: thesis: S1[x,h]
take g ; :: thesis: ex h being Function st
( 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 ) ) ) ) ) )
take h ; :: thesis: ( 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 ) ) ) ) ) )
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 A9, A12; :: thesis: verum
end;
consider f being Function such that
A13: ( dom f = Funcs b,a & ( for x being set st x in Funcs b,a holds
S1[x,f . x] ) ) from CLASSES1:sch 1(A8);
 deffunc H1( set ) -> set = Funcs b,$1;
consider F being Function such that
A14: ( dom F = dom (b -powerfunc_of a) & ( for x being set st x in dom (b -powerfunc_of a) holds
F . x = H1(x) ) ) from FUNCT_1:sch 3();
 A15: rng f c= Funcs (cf a),(Union (disjoin F))
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Funcs (cf a),(Union (disjoin F)) )
assume y in rng f ; :: thesis: y in Funcs (cf a),(Union (disjoin F))
then consider x being set such that
A16: x in dom f and
A17: y = f . x by FUNCT_1:def 5;
consider g, h being Function such that
g = x and
A18: h = f . x and
dom g = b and
rng g c= a and
A19: dom h = cf a and
A20: 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 A13, A16;
rng h c= Union (disjoin F)
proof
let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in rng h or x1 in Union (disjoin F) )
assume x1 in rng h ; :: thesis: x1 in Union (disjoin F)
then consider x2 being set such that
A21: x2 in dom h and
A22: x1 = h . x2 by FUNCT_1:def 5;
consider fx being Function such that
A23: x1 = [fx,(phi . x2)] and
A24: dom fx = b and
A25: 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 A19, A20, A21, A22;
rng fx c= phi . x2
proof
reconsider x2 = x2 as Ordinal by A19, A21;
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng fx or z in phi . x2 )
reconsider A = phi . x2 as Ordinal ;
assume z in rng fx ; :: thesis: z in phi . x2
then consider z9 being set such that
A26: ( z9 in dom fx & z = fx . z9 ) by FUNCT_1:def 5;
A27: ( ( z = g . z9 & g . z9 in phi . x2 ) or z = 0 ) by A24, A25, A26;
A <> 0 by A3, A7, A19, A21, FUNCT_1:def 5;
hence z in phi . x2 by A27, ORDINAL3:10; :: thesis: verum
end;
then A28: fx in Funcs b,(phi . x2) by A24, FUNCT_2:def 2;
A29: ( [fx,(phi . x2)] `1 = fx & [fx,(phi . x2)] `2 = phi . x2 ) by MCART_1:7;
( phi . x2 in rng phi & phi . x2 is Cardinal ) by A3, A6, A19, A21, CARD_3:def 1, FUNCT_1:def 5;
then A30: phi . x2 in dom (b -powerfunc_of a) by A4, Def3;
then F . (phi . x2) = Funcs b,(phi . x2) by A14;
hence x1 in Union (disjoin F) by A14, A23, A28, A30, A29, CARD_3:33; :: thesis: verum
end;
hence y in Funcs (cf a),(Union (disjoin F)) by A17, A18, A19, FUNCT_2:def 2; :: thesis: verum
end;
( card (card (Union (disjoin F))) = card (Union (disjoin F)) & card (cf a) = cf a ) by CARD_1:def 5;
then A31: 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 ;
A32: dom (Card F) = dom F by CARD_3:def 2;
A33: f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b1 being set holds
( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 )
let y be set ; :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A34: x in dom f and
A35: y in dom f and
A36: f . x = f . y ; :: thesis: x = y
consider g1, h1 being Function such that
A37: g1 = x and
A38: h1 = f . x and
A39: dom g1 = b and
A40: rng g1 c= a and
dom h1 = cf a and
A41: 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 A13, A34;
consider g2, h2 being Function such that
A42: g2 = y and
A43: h2 = f . y and
A44: dom g2 = b and
A45: rng g2 c= a and
dom h2 = cf a and
A46: 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 A13, A35;
now
let x1 be set ; :: thesis: ( x1 in b implies g1 . x1 = g2 . x1 )
assume x1 in b ; :: thesis: g1 . x1 = g2 . x1
then reconsider X = x1 as Element of b ;
( g1 . X in rng g1 & g2 . X in rng g2 ) by A39, A44, FUNCT_1:def 5;
then reconsider A1 = g1 . x1, A2 = g2 . x1 as Element of a by A40, A45;
set A = A1 \/ A2;
( A1 \/ A2 = A1 or A1 \/ A2 = A2 ) by ORDINAL3:15;
then succ (A1 \/ A2) in a by ORDINAL1:41;
then consider B being Ordinal such that
A47: B in rng phi and
A48: succ (A1 \/ A2) c= B by A5, ORDINAL2:29;
consider x2 being set such that
A49: x2 in dom phi and
A50: B = phi . x2 by A47, FUNCT_1:def 5;
A51: A1 \/ A2 in succ (A1 \/ A2) by ORDINAL1:10;
then A52: A2 in B by A48, ORDINAL1:22, XBOOLE_1:7;
consider f1 being Function such that
A53: h1 . x2 = [f1,(phi . x2)] and
dom f1 = b and
A54: 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, A41, A49;
A1 in B by A48, A51, ORDINAL1:22, XBOOLE_1:7;
then A55: f1 . X = g1 . x1 by A50, A54;
consider f2 being Function such that
A56: h2 . x2 = [f2,(phi . x2)] and
dom f2 = b and
A57: 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, A46, A49;
f1 = f2 by A36, A38, A43, A53, A56, ZFMISC_1:33;
hence g1 . x1 = g2 . x1 by A50, A57, A52, A55; :: thesis: verum
end;
hence x = y by A37, A39, A42, A44, FUNCT_1:9; :: thesis: verum
end;
A58: dom (disjoin F) = dom F by CARD_3:def 3;
A59: now
let x be set ; :: thesis: ( x in dom F implies (Card (disjoin F)) . x = (Card F) . x )
assume A60: x in dom F ; :: thesis: (Card (disjoin F)) . x = (Card F) . x
then A61: (disjoin F) . x = [:(F . x),{x}:] by CARD_3:def 3;
( (Card F) . x = card (F . x) & (Card (disjoin F)) . x = card ((disjoin F) . x) ) by A58, A60, CARD_3:def 2;
hence (Card (disjoin F)) . x = (Card F) . x by A61, CARD_2:13; :: thesis: verum
end;
now
let x be set ; :: thesis: ( x in dom F implies (Card F) . x = (b -powerfunc_of a) . x )
assume A62: x in dom F ; :: thesis: (Card F) . x = (b -powerfunc_of a) . x
then reconsider M = x as Cardinal by A14, Def3;
M in a by A14, A62, Def3;
then A63: (b -powerfunc_of a) . M = exp M,b by Def3;
( (Card F) . x = card (F . x) & F . x = Funcs b,x ) by A14, A62, CARD_3:def 2;
hence (Card F) . x = (b -powerfunc_of a) . x by A63, CARD_2:def 3; :: thesis: verum
end;
then A64: Card F = b -powerfunc_of a by A14, A32, FUNCT_1:9;
dom (Card (disjoin F)) = dom (disjoin F) by CARD_3:def 2;
then Card F = Card (disjoin F) by A58, A32, A59, FUNCT_1:9;
then card (Union (disjoin F)) c= Sum (b -powerfunc_of a) by A64, CARD_3:54;
then A65: exp (card (Union (disjoin F))),(cf a) c= exp (Sum (b -powerfunc_of a)),(cf a) by CARD_3:139;
exp a,b = card (Funcs b,a) by CARD_2:def 3;
then exp a,b c= card (Funcs (cf a),(Union (disjoin F))) by A13, A33, A15, CARD_1:26;
then A66: ( exp (exp a,b),(cf a) = exp a,(b *` (cf a)) & exp a,b c= exp (Sum (b -powerfunc_of a)),(cf a) ) by A31, A65, CARD_2:43, XBOOLE_1:1;
Sum (b -powerfunc_of a) c= exp a,b by Th45;
then A67: exp (Sum (b -powerfunc_of a)),(cf a) c= exp (exp a,b),(cf a) by CARD_3:139;
b *` (cf a) = b by A1, Th27;
hence exp a,b = exp (Sum (b -powerfunc_of a)),(cf a) by A67, A66, XBOOLE_0:def 10; :: thesis: verum