theorem Th44: :: ORDINAL2:44

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