theorem Th4: :: ORDINAL7:4

for a being Ordinal holds a *^ a = exp (a,2)