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 A1: ( (C1 *^ A) +^ D1 = (C2 *^ A) +^ D2 & D1 in A & D2 in A ) ; :: thesis: ( C1 = C2 & D1 = D2 )
set B = (C1 *^ A) +^ D1;

A2: now

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

end;

now

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

end;

hence C1 = C2 by A2, ORDINAL1:24; :: thesis: D1 = D2
hence D1 = D2 by A1, Th24; :: thesis: verum