let b, a 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 set ; :: 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:5;
Sum (a --> (exp a,b)) = a *` (exp a,b) by CARD_3:52;
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:46;
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 } by FUNCOP_1:19; :: 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 set ; :: 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 Def3;
hence x in { c where c is Element of a : c is Cardinal } ; :: thesis: verum

end;

let x be set ; :: 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 Def3; :: thesis: verum

end;

( 1 in b & exp a,1 = a ) by Lm1, Th25, CARD_2:40;
then a c= exp a,b by CARD_3:139;
then A4: a *` (exp a,b) = exp a,b by Th27;

now

let x be set ; :: 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:13;
(b -powerfunc_of a) . x = exp c,b by A6, Def3;
hence (b -powerfunc_of a) . x c= ({ c where c is Element of a : c is Cardinal } --> (exp a,b)) . x by A8, CARD_3:139; :: 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:43;
hence Sum (b -powerfunc_of a) c= exp a,b by A2, A4, XBOOLE_1:1; :: thesis: verum