let B, C be complex-membered set ; :: thesis: for a being complex number holds a ** (B -- C) = (a ** B) -- (a ** C)
let a be complex number ; :: thesis: a ** (B -- C) = (a ** B) -- (a ** C)
thus a ** (B -- C) = (a ** B) ++ (a ** (-- C)) by Th214
.= (a ** B) -- (a ** C) by Th100 ; :: thesis: verum