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