let A, B, C, D be Ordinal; :: thesis: ( A in B & ( ( C c= D & D <> {} ) or C in D ) implies A *^ C in B *^ D )
assume that
A1: A in B and
A2: ( ( C c= D & D <> {} ) or C in D ) ; :: thesis: A *^ C in B *^ D
A3: C c= D by A2, ORDINAL1:def 2;
A *^ D in B *^ D by A1, A2, ORDINAL2:57;
hence A *^ C in B *^ D by A3, ORDINAL1:22, ORDINAL2:59; :: thesis: verum