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)
thus a /// (A \ B) = a ** ((A "") \ (B "")) by Th34
.= (a ** (A "")) \ (a ** (B "")) by A1, Th199
.= (a /// A) \ (a /// B) ; :: thesis: verum