let A, B be complex-membered set ; :: thesis: for a being complex number st a <> 0 holds
a ** (A \ B) = (a ** A) \ (a ** B)
let a be complex number ; :: thesis: ( a <> 0 implies a ** (A \ B) = (a ** A) \ (a ** B) )
assume A1: a <> 0 ; :: thesis: a ** (A \ B) = (a ** A) \ (a ** B)
let z be complex number ; :: 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 Element of COMPLEX such that
A2: z = a * c and
A3: c in A \ B by Th201;
A4: a * c in a ** A by A3, Th199;

now

assume a * c in a ** B ; :: thesis: contradiction
then consider c1 being Element of COMPLEX such that
A5: a * c = a * c1 and
A6: c1 in B by Th201;
c = c1 by A1, A5, XCMPLX_1:5;
hence contradiction by A3, A6, XBOOLE_0:def 5; :: thesis: verum

end;

hence z in (a ** A) \ (a ** B) by A2, A4, XBOOLE_0:def 5; :: thesis: verum

end;

assume A7: z in (a ** A) \ (a ** B) ; :: thesis: z in a ** (A \ B)
then consider c being Element of COMPLEX such that
A8: z = a * c and
A9: c in A by Th201;

now

assume not c in A \ B ; :: thesis: contradiction
then c in B by A9, XBOOLE_0:def 5;
then a * c in a ** B by Th199;
hence contradiction by A7, A8, XBOOLE_0:def 5; :: thesis: verum

end;

hence z in a ** (A \ B) by A8, Th199; :: thesis: verum