let A, B be complex-membered set ; :: thesis: (A \+\ B) "" = (A "") \+\ (B "")
thus (A \+\ B) "" = ((A \ B) "") \/ ((B \ A) "") by Th32
.= ((A "") \ (B "")) \/ ((B \ A) "") by Th34
.= (A "") \+\ (B "") by Th34 ; :: thesis: verum