theorem Th28: :: ORDINAL2:28

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