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

per cases ( ( 1 in b & 0 in a & 0 in c ) or not 1 in b or not 0 in a or not 0 in c ) ;

suppose A2: ( 1 in b & 0 in a & 0 in c ) ; :: thesis: b -exponent a c= b -exponent c

then exp (b,(b -exponent a)) c= a by ORDINAL5:def 10;
then exp (b,(b -exponent a)) c= c by A1, XBOOLE_1:1;
hence b -exponent a c= b -exponent c by A2, ORDINAL5:def 10; :: thesis: verum

end;

suppose not 1 in b ; :: thesis: b -exponent a c= b -exponent c

then ( b -exponent a = 0 & b -exponent c = 0 ) by ORDINAL5:def 10;
hence b -exponent a c= b -exponent c ; :: thesis: verum

end;

suppose ( not 0 in a or not 0 in c ) ; :: thesis: b -exponent a c= b -exponent c

then not 0 in a by A1;
then b -exponent a = {} by ORDINAL5:def 10;
hence b -exponent a c= b -exponent c ; :: thesis: verum

end;

end;