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

A1: now

assume A2: not B c= A ; :: thesis: (A *^ C) -^ (B *^ C) = (A -^ B) *^ C
then A3: ( not B *^ C c= A *^ C or C = {} ) by Th38;
A4: {} *^ C = {} by ORDINAL2:35;
A5: A *^ {} = {} by ORDINAL2:38;
A -^ B = {} by A2, Def6;
hence (A *^ C) -^ (B *^ C) = (A -^ B) *^ C by A3, A5, A4, Def6, Th69; :: thesis: verum

end;

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;

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