let A, B, C, D be Ordinal; :: thesis: ( A c= B & C c= D implies A *^ C c= B *^ D )
assume that
A1: A c= B and
A2: C c= D ; :: thesis: A *^ C c= B *^ D
A3: B *^ C c= B *^ D by A2, ORDINAL2:42;
A *^ C c= B *^ C by A1, ORDINAL2:41;
hence A *^ C c= B *^ D by A3; :: thesis: verum