theorem :: CARD_5:34

for a, b being Aleph st a is limit_cardinal & b in cf a holds
exp (a,b) = Sum (b -powerfunc_of a)