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