let A, B, C be Ordinal; :: thesis: ( B *^ A = C *^ A & A <> {} implies B = C )
assume that
A1: B *^ A = C *^ A and
A2: A <> {} and
A3: B <> C ; :: thesis: contradiction
( B in C or C in B ) by A3, ORDINAL1:14;
then B *^ A in B *^ A by A1, A2, ORDINAL2:40;
hence contradiction ; :: thesis: verum