let A, B, C be Ordinal; :: thesis: (A *^ C) -^ (B *^ C) = (A -^ B) *^ C
A1: now :: thesis: ( not B c= A implies (A *^ C) -^ (B *^ C) = (A -^ B) *^ C )
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 Th35;
A4: {} *^ C = {} by ORDINAL2:35;
A5: A *^ {} = {} by ORDINAL2:38;
A -^ B = {} by A2, Def5;
hence (A *^ C) -^ (B *^ C) = (A -^ B) *^ C by A3, A5, A4, Def5, Th56; :: thesis: verum
end;
now :: thesis: ( B c= A implies (A *^ C) -^ (B *^ C) = (A -^ B) *^ C )
assume B c= A ; :: thesis: (A *^ C) -^ (B *^ C) = (A -^ B) *^ C
then A = B +^ (A -^ B) by Def5;
then A *^ C = (B *^ C) +^ ((A -^ B) *^ C) by Th46;
hence (A *^ C) -^ (B *^ C) = (A -^ B) *^ C by Th52; :: thesis: verum
end;
hence (A *^ C) -^ (B *^ C) = (A -^ B) *^ C by A1; :: thesis: verum