for A being Ordinal holds
( exp (A,1) = A & exp (1,A) = 1 )