theorem Th31: :: ORDINAL5:31

for a being Ordinal st 0 in a holds
exp (a,(a |^|^ omega)) = a |^|^ omega