let a, b be Ordinal; :: thesis: ( omega -exponent a in omega -exponent b implies b -^ a = b )
assume A1: omega -exponent a in omega -exponent b ; :: thesis: b -^ a = b

per cases ( a = 0 or a <> 0 ) ;

suppose a = 0 ; :: thesis: b -^ a = b

hence b -^ a = b by ORDINAL3:56; :: thesis: verum

end;

suppose A2: a <> 0 ; :: thesis: b -^ a = b

A3: ( 1 in omega & 0 in b ) by A1, ORDINAL5:def 10;
then omega *^ a c= b by A1, A2, Th103;
then A4: a +^ b = b by Th30;
A5: a in exp (omega,(omega -exponent b)) by A1, Th102;
exp (omega,(omega -exponent b)) c= b by A3, ORDINAL5:def 10;
then a c= b by A5, ORDINAL1:def 2;
hence b -^ a = b by A4, ORDINAL3:def 5; :: thesis: verum

end;

end;