theorem Th88: :: ORDINAL7:75

for a being Ordinal
for n being Nat holds a (+) n = a +^ n