theorem :: ORDINAL4:31

for A, B, C being Ordinal holds exp ((exp (C,A)),B) = exp (C,(B *^ A))