theorem :: CARD_5:32
for a, b being Aleph holds exp ((nextcard a),b) = (exp (a,b)) *` (nextcard a)