for a being ordinal number
for n1, n2 being natural number st n1 <> n2 holds
a +^ n1 <> a +^ n2 by ORDINAL3:21;