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

A4: now :: thesis: not C2 in C1

assume C2 in C1 ; :: thesis: contradiction
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: verum

end;

now :: thesis: not C1 in C2

assume C1 in C2 ; :: thesis: contradiction
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: verum

end;

hence C1 = C2 by A4, ORDINAL1:14; :: thesis: D1 = D2
hence D1 = D2 by A1, Th21; :: thesis: verum