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