let A, B, C be Ordinal; :: thesis: ( A c= B implies C +^ A c= C +^ B )
assume A1: A c= B ; :: thesis: C +^ A c= C +^ B

now

assume A <> B ; :: thesis: C +^ A c= C +^ B
then A c< B by A1, XBOOLE_0:def 8;
then C +^ A in C +^ B by Th49, ORDINAL1:21;
hence C +^ A c= C +^ B by ORDINAL1:def 2; :: thesis: verum

end;

hence C +^ A c= C +^ B ; :: thesis: verum