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 Th16
.= (a ++ (-- A)) /\ (a ++ (-- B)) by Th149
.= (a -- A) /\ (a -- B) ; :: thesis: verum