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