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