let A, B be complex-membered set ; :: thesis: for a being Complex st a <> 0 holds
a ** (A \ B) = (a ** A) \ (a ** B)
let a be Complex; :: 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; :: 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
A2: z = a * c and
A3: c in A \ B by Th195;

A4: now :: thesis: not a * c in a ** B

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

end;

a * c in a ** A by A3, Th193;
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 Complex such that
A8: z = a * c and
A9: c in A by Th195;

now :: thesis: c in A \ B

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 Th193;
hence contradiction by A7, A8, XBOOLE_0:def 5; :: thesis: verum

end;

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