theorem Th42: :: ORDINAL5:42

for a being Ordinal holds epsilon_ (succ a) = (epsilon_ a) |^|^ omega