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