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);
A1: { 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;

A2: 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 A3: 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
A4: ( x = c & c is Cardinal ) ;
reconsider c = c as Cardinal by A4;
( ({ c where c is Element of a : c is Cardinal } --> (exp a,b)) . x = exp a,b & (b -powerfunc_of a) . x = exp c,b & exp c,b c= exp a,b ) by A3, A4, Def3, CARD_3:139, FUNCOP_1:13;
hence (b -powerfunc_of a) . x c= ({ c where c is Element of a : c is Cardinal } --> (exp a,b)) . x ; :: thesis: verum

end;

A5: ( 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 & a <> 0 & exp a,1 = a ) by Lm1, Th25, CARD_2:40;
then ( { c where c is Element of a : c is Cardinal } --> (exp a,b) c= a --> (exp a,b) & a c= exp a,b & Sum (a --> (exp a,b)) = a *` (exp a,b) ) by A1, CARD_3:52, CARD_3:139, FUNCT_4:5;
then ( Sum (b -powerfunc_of a) c= Sum ({ c where c is Element of a : c is Cardinal } --> (exp a,b)) & Sum ({ c where c is Element of a : c is Cardinal } --> (exp a,b)) c= a *` (exp a,b) & a *` (exp a,b) = exp a,b ) by A2, A5, Th27, CARD_3:43, CARD_3:46;
hence Sum (b -powerfunc_of a) c= exp a,b by XBOOLE_1:1; :: thesis: verum