let A, B, C be Ordinal; :: thesis: ( A c= B implies A *^ C c= B *^ C )
assume A1: A c= B ; :: thesis: A *^ C c= B *^ C

A2: now :: thesis: ( C <> {} implies A *^ C c= B *^ C )

assume A3: C <> {} ; :: thesis: A *^ C c= B *^ C

now :: thesis: ( A <> B implies A *^ C c= B *^ C )

assume A <> B ; :: thesis: A *^ C c= B *^ C
then A c< B by A1, XBOOLE_0:def 8;
then A *^ C in B *^ C by A3, Th40, ORDINAL1:11;
hence A *^ C c= B *^ C by ORDINAL1:def 2; :: thesis: verum

end;

hence A *^ C c= B *^ C ; :: thesis: verum

end;

now :: thesis: ( C = {} implies A *^ C c= B *^ C )

assume C = {} ; :: thesis: A *^ C c= B *^ C
then A *^ C = {} by Th38;
hence A *^ C c= B *^ C ; :: thesis: verum

end;

hence A *^ C c= B *^ C by A2; :: thesis: verum