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