let A, C, B be Ordinal; :: thesis: (A *^ C) -^ (B *^ C) = (A -^ B) *^ C

A1: now

assume B c= A ; :: thesis: (A *^ C) -^ (B *^ C) = (A -^ B) *^ C
then A = B +^ (A -^ B) by Def6;
then A *^ C = (B *^ C) +^ ((A -^ B) *^ C) by Th54;
hence (A *^ C) -^ (B *^ C) = (A -^ B) *^ C by Th65; :: thesis: verum

end;

now

assume not B c= A ; :: thesis: (A *^ C) -^ (B *^ C) = (A -^ B) *^ C
then ( A -^ B = {} & ( not B *^ C c= A *^ C or C = {} ) & A *^ {} = {} & {} *^ C = {} ) by Def6, Th38, ORDINAL2:52, ORDINAL2:55;
hence (A *^ C) -^ (B *^ C) = (A -^ B) *^ C by Def6, Th69; :: thesis: verum

end;

hence (A *^ C) -^ (B *^ C) = (A -^ B) *^ C by A1; :: thesis: verum