theorem :: CARD_5:35

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