let F, G be ext-real-membered set ; :: thesis: for r being real number holds r -- (F \+\ G) = (r -- F) \+\ (r -- G)
let r be real number ; :: thesis: r -- (F \+\ G) = (r -- F) \+\ (r -- G)
thus r -- (F \+\ G) = r ++ ((-- F) \+\ (-- G)) by Th8
.= (r ++ (-- F)) \+\ (r ++ (-- G)) by Th140
.= (r -- F) \+\ (r -- G) ; :: thesis: verum