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