let a, b be Aleph; :: thesis: Sum (b -powerfunc_of a) c= exp (a,b)
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

proof

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

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 } )

proof

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: dom (b -powerfunc_of a) = { c where c is Element of a : c is Cardinal }
thus dom (b -powerfunc_of a) c= { c where c is Element of a : c is Cardinal } :: according to XBOOLE_0:def 10 :: thesis: { c where c is Element of a : c is Cardinal } c= dom (b -powerfunc_of a)

proof

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

end;

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

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;

now :: thesis: for x being object st x in { c where c is Element of a : c is Cardinal } holds
(b -powerfunc_of a) . x c= ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x

let x be object ; :: thesis: ( x in { c where c is Element of a : c is Cardinal } implies (b -powerfunc_of a) . x c= ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x )
assume A5: x in { c where c is Element of a : c is Cardinal } ; :: thesis: (b -powerfunc_of a) . x c= ( { c where c is Element of a : c is Cardinal } --> (exp (a,b))) . x
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: verum

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: verum