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:40;
hence A *^ C in B *^ D by A3, ORDINAL1:12, ORDINAL2:42; :: thesis: verum