for a, b being Aleph holds Sum (b -powerfunc_of a) c= exp (a,b)