let A, B, C, D be Ordinal; :: thesis: ( A c= B & C c= D implies A +^ C c= B +^ D )
assume that
A1: A c= B and
A2: C c= D ; :: thesis: A +^ C c= B +^ D
A3: B +^ C c= B +^ D by A2, ORDINAL2:33;
A +^ C c= B +^ C by A1, ORDINAL2:34;
hence A +^ C c= B +^ D by A3; :: thesis: verum