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)) \/ (r ++ (G \ F)) by Th41
.= ((r ++ F) \ (r ++ G)) \/ (r ++ (G \ F)) by Th139
.= (r ++ F) \+\ (r ++ G) by Th139 ; :: thesis: verum