theorem Th36: :: ORDINAL2:36

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