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

assume C2 in C1 ; :: thesis: contradiction
then consider C being Ordinal such that
A5: C1 = C2 +^ C and
A6: C <> {} by Th31;
(C1 *^ A) +^ D1 = ((C2 *^ A) +^ (C *^ A)) +^ D1 by A5, Th54
.= (C2 *^ A) +^ ((C *^ A) +^ D1) by Th33 ;
then A7: D2 = (C *^ A) +^ D1 by A1, Th24;
A8: C *^ A c= (C *^ A) +^ D1 by Th27;
A c= C *^ A by A6, Th39;
hence contradiction by A3, A7, A8, ORDINAL1:5; :: thesis: verum

end;

now

assume C1 in C2 ; :: thesis: contradiction
then consider C being Ordinal such that
A9: C2 = C1 +^ C and
A10: C <> {} by Th31;
(C1 *^ A) +^ D1 = ((C1 *^ A) +^ (C *^ A)) +^ D2 by A1, A9, Th54
.= (C1 *^ A) +^ ((C *^ A) +^ D2) by Th33 ;
then A11: D1 = (C *^ A) +^ D2 by Th24;
A12: C *^ A c= (C *^ A) +^ D2 by Th27;
A c= C *^ A by A10, Th39;
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, Th24; :: thesis: verum