let A be Ordinal; :: thesis:
let C1, D1, C2, D2 be Ordinal; :: thesis:
assume that
A1: (C1 *^ A) +^ D1 = (C2 *^ A) +^ D2 and
A2: D1 in A and
A3: D2 in A ; :: thesis:
set B = (C1 *^ A) +^ D1;

assume C2 in C1 ; :: thesis:
then consider C being Ordinal such that
A5: C1 = C2 +^ C and
A6: C <> {} by Th28;
(C1 *^ A) +^ D1 = ((C2 *^ A) +^ (C *^ A)) +^ D1 by A5, Th46
.= (C2 *^ A) +^ ((C *^ A) +^ D1) by Th30 ;
then A7: D2 = (C *^ A) +^ D1 by A1, Th21;
A8: C *^ A c= (C *^ A) +^ D1 by Th24;
A c= C *^ A by A6, Th36;
hence contradiction by A3, A7, A8, ORDINAL1:5; :: thesis:

end;

assume C1 in C2 ; :: thesis:
then consider C being Ordinal such that
A9: C2 = C1 +^ C and
A10: C <> {} by Th28;
(C1 *^ A) +^ D1 = ((C1 *^ A) +^ (C *^ A)) +^ D2 by A1, A9, Th46
.= (C1 *^ A) +^ ((C *^ A) +^ D2) by Th30 ;
then A11: D1 = (C *^ A) +^ D2 by Th21;
A12: C *^ A c= (C *^ A) +^ D2 by Th24;
A c= C *^ A by A10, Th36;
hence contradiction by A2, A11, A12, ORDINAL1:5; :: thesis:

end;