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