theorem Th81: :: ORDINAL7:68

for a, b, c being Ordinal holds (a (+) b) (+) c = a (+) (b (+) c)