let A, B be Ordinal; ( B <> {} implies ( A c= A *^ B & A c= B *^ A ) )
assume
B <> {}
; ( A c= A *^ B & A c= B *^ A )
then
{} in B
by Th8;
then A1:
1 c= B
by Lm1, ORDINAL1:21;
then A2:
A *^ 1 c= A *^ B
by ORDINAL2:42;
1 *^ A c= B *^ A
by A1, ORDINAL2:41;
hence
( A c= A *^ B & A c= B *^ A )
by A2, ORDINAL2:39; verum