theorem Th140: :: MEMBER_1:140

for F, G being ext-real-membered set
for r being Real holds r ++ (F \+\ G) = (r ++ F) \+\ (r ++ G)