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, Th28, ORDINAL1:12;
defpred S₁[ object , object ] 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 object st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being object 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 object st x in Funcs (b,a) holds
ex x1 being object st S₁[x,x1]

proof

let x be object ; :: thesis: ( x in Funcs (b,a) implies ex x1 being object st S₁[x,x1] )
assume x in Funcs (b,a) ; :: thesis: ex x1 being object st S₁[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 S₂[ object , object ] means ex fx being Function st
( $2 = [fx,(phi . $1)] & dom fx = b & ( for z being object 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 object st y in cf a holds
ex x2 being object st S₂[y,x2]

proof

deffunc H₁( object ) -> Element of omega = 0 ;
deffunc H₂( object ) -> set = g . $1;
let y be object ; :: thesis: ( y in cf a implies ex x2 being object st S₂[y,x2] )
assume y in cf a ; :: thesis: ex x2 being object st S₂[y,x2]
defpred S₃[ object ] means g . $1 in phi . y;
consider fx being Function such that
A11: ( dom fx = b & ( for z being object 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: S₂[y,[fx,(phi . y)]]
take fx ; :: thesis: ( [fx,(phi . y)] = [fx,(phi . y)] & dom fx = b & ( for z being object 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 object 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 object st y in cf a holds
S₂[y,h . y] ) ) from CLASSES1:sch 1(A10);
take h ; :: thesis: S₁[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 object st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being object 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 object st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being object 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 object st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being object 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 object st x in Funcs (b,a) holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A8);
deffunc H₁( 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 = H₁(x) ) ) from FUNCT_1:sch 5();
A15: rng f c= Funcs ((cf a),(Union (disjoin F)))

proof

let y be object ; :: 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 object such that
A16: x in dom f and
A17: y = f . x by FUNCT_1:def 3;
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 object st y in cf a holds
ex fx being Function st
( h . y = [fx,(phi . y)] & dom fx = b & ( for z being object 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 object ; :: 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 object such that
A21: x2 in dom h and
A22: x1 = h . x2 by FUNCT_1:def 3;
consider fx being Function such that
A23: x1 = [fx,(phi . x2)] and
A24: dom fx = b and
A25: for z being object 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 object ; :: 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 object such that
A26: ( z9 in dom fx & z = fx . z9 ) by FUNCT_1:def 3;
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 3;
hence z in phi . x2 by A27, ORDINAL3:8; :: 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 ) ;
( phi . x2 in rng phi & phi . x2 is Cardinal ) by A3, A6, A19, A21, CARD_3:def 1, FUNCT_1:def 3;
then A30: phi . x2 in dom (b -powerfunc_of a) by A4, Def2;
then F . (phi . x2) = Funcs (b,(phi . x2)) by A14;
hence x1 in Union (disjoin F) by A14, A23, A28, A30, A29, CARD_3:22; :: 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 ) ;
then A31: card (Funcs ((cf a),(Union (disjoin F)))) = card (Funcs ((cf a),(card (Union (disjoin F))))) by FUNCT_5:61
.= 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, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom 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 object st x1 in cf a holds
ex fx being Function st
( h1 . x1 = [fx,(phi . x1)] & dom fx = b & ( for z being object 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 object st x2 in cf a holds
ex fx being Function st
( h2 . x2 = [fx,(phi . x2)] & dom fx = b & ( for z being object 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 :: thesis: for x1 being object st x1 in b holds
g1 . x1 = g2 . x1

let x1 be object ; :: 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 3;
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:12;
then succ (A1 \/ A2) in a by ORDINAL1:28;
then consider B being Ordinal such that
A47: B in rng phi and
A48: succ (A1 \/ A2) c= B by A5, ORDINAL2:21;
consider x2 being object such that
A49: x2 in dom phi and
A50: B = phi . x2 by A47, FUNCT_1:def 3;
A51: A1 \/ A2 in succ (A1 \/ A2) by ORDINAL1:6;
then A52: A2 in B by A48, ORDINAL1:12, XBOOLE_1:7;
consider f1 being Function such that
A53: h1 . x2 = [f1,(phi . x2)] and
dom f1 = b and
A54: for z being object 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:12, 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 object 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, XTUPLE_0:1;
hence g1 . x1 = g2 . x1 by A50, A57, A52, A55; :: thesis: verum

end;

hence x = y by A37, A39, A42, A44, FUNCT_1:2; :: thesis: verum

end;

A58: dom (disjoin F) = dom F by CARD_3:def 3;

A59: now :: thesis: for x being object st x in dom F holds
(Card (disjoin F)) . x = (Card F) . x

let x be object ; :: 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_1:69; :: thesis: verum

end;

now :: thesis: for x being object st x in dom F holds
(Card F) . x = (b -powerfunc_of a) . x

let x be object ; :: 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, Def2;
M in a by A14, A62, Def2;
then A63: (b -powerfunc_of a) . M = exp (M,b) by Def2;
reconsider xx = x as set by TARSKI:1;
( (Card F) . x = card (F . x) & F . x = Funcs (b,xx) ) 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;
dom (Card (disjoin F)) = dom (disjoin F) by CARD_3:def 2;
then Card F = Card (disjoin F) by A58, A32, A59;
then card (Union (disjoin F)) c= Sum (b -powerfunc_of a) by A64, CARD_3:39;
then A65: exp ((card (Union (disjoin F))),(cf a)) c= exp ((Sum (b -powerfunc_of a)),(cf a)) by CARD_2:93;
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:10;
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:30;
Sum (b -powerfunc_of a) c= exp (a,b) by Th32;
then A67: exp ((Sum (b -powerfunc_of a)),(cf a)) c= exp ((exp (a,b)),(cf a)) by CARD_2:93;
b *` (cf a) = b by A1, Th17;
hence exp (a,b) = exp ((Sum (b -powerfunc_of a)),(cf a)) by A67, A66; :: thesis: verum