let A, B be complex-membered set ; :: thesis: for a being Complex holds a -- (A \+\ B) = (a -- A) \+\ (a -- B)
let a be Complex; :: thesis: a -- (A \+\ B) = (a -- A) \+\ (a -- B)
thus a -- (A \+\ B) = a ++ ((-- A) \+\ (-- B)) by Th18
.= (a ++ (-- A)) \+\ (a ++ (-- B)) by Th151
.= (a -- A) \+\ (a -- B) ; :: thesis: verum