let a, b be Aleph; :: thesis:
set X = { c where c is Element of a : c is Cardinal } ;
set f = { c where c is Element of a : c is Cardinal } --> (exp (a,b));
{ c where c is Element of a : c is Cardinal } c= a

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { c where c is Element of a : c is Cardinal } ; :: thesis:
then ex c being Element of a st
( x = c & c is Cardinal ) ;
hence x in a ; :: thesis:

end;

then A1: { c where c is Element of a : c is Cardinal } --> (exp (a,b)) c= a --> (exp (a,b)) by FUNCT_4:4;
Sum (a --> (exp (a,b))) = a *` (exp (a,b)) by CARD_2:65;
then A2: Sum ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) c= a *` (exp (a,b)) by A1, CARD_3:33;
A3: ( dom ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) = { c where c is Element of a : c is Cardinal } & dom (b -powerfunc_of a) = { c where c is Element of a : c is Cardinal } )

thus dom ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) = { c where c is Element of a : c is Cardinal } ; :: thesis:
thus dom (b -powerfunc_of a) c= { c where c is Element of a : c is Cardinal } :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in dom (b -powerfunc_of a) ; :: thesis:
then ( x in a & x is Cardinal ) by Def2;
hence x in { c where c is Element of a : c is Cardinal } ; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { c where c is Element of a : c is Cardinal } ; :: thesis:
then ex c being Element of a st
( x = c & c is Cardinal ) ;
hence x in dom (b -powerfunc_of a) by Def2; :: thesis:

end;

( 1 in b & exp (a,1) = a ) by Lm1, Th15, CARD_2:27;
then a c= exp (a,b) by CARD_2:93;
then A4: a *` (exp (a,b)) = exp (a,b) by Th17;

let x be object ; :: thesis:
assume A5: x in { c where c is Element of a : c is Cardinal } ; :: thesis:
then consider c being Element of a such that
A6: x = c and
A7: c is Cardinal ;
reconsider c = c as Cardinal by A7;
A8: ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x = exp (a,b) by A5, FUNCOP_1:7;
(b -powerfunc_of a) . x = exp (c,b) by A6, Def2;
hence (b -powerfunc_of a) . x c= ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x by A8, CARD_2:93; :: thesis:

end;

then Sum (b -powerfunc_of a) c= Sum ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) by A3, CARD_3:30;
hence Sum (b -powerfunc_of a) c= exp (a,b) by A2, A4; :: thesis: