let A, B be complex-membered set ; :: thesis: for a being Complex holds a ++ (A \ B) = (a ++ A) \ (a ++ B)
let a be Complex; :: thesis: a ++ (A \ B) = (a ++ A) \ (a ++ B)
let z be Complex; :: according to MEMBERED:def 13 :: thesis: ( ( not z in a ++ (A \ B) or z in (a ++ A) \ (a ++ B) ) & ( not z in (a ++ A) \ (a ++ B) or z in a ++ (A \ B) ) )
hereby :: thesis: ( not z in (a ++ A) \ (a ++ B) or z in a ++ (A \ B) )
assume z in a ++ (A \ B) ; :: thesis: z in (a ++ A) \ (a ++ B)
then consider c being Complex such that
A1: z = a + c and
A2: c in A \ B by Th143;
A3: now :: thesis: not a + c in a ++ B
assume a + c in a ++ B ; :: thesis: contradiction
then ex c1 being Complex st
( a + c = a + c1 & c1 in B ) by Th143;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum
end;
a + c in a ++ A by A2, Th141;
hence z in (a ++ A) \ (a ++ B) by A1, A3, XBOOLE_0:def 5; :: thesis: verum
end;
assume A4: z in (a ++ A) \ (a ++ B) ; :: thesis: z in a ++ (A \ B)
then consider c being Complex such that
A5: z = a + c and
A6: c in A by Th143;
now :: thesis: c in A \ B
assume not c in A \ B ; :: thesis: contradiction
then c in B by A6, XBOOLE_0:def 5;
then a + c in a ++ B by Th141;
hence contradiction by A4, A5, XBOOLE_0:def 5; :: thesis: verum
end;
hence z in a ++ (A \ B) by A5, Th141; :: thesis: verum