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