theorem Th133: :: MEMBER_1:133

for F being ext-real-membered set
for f being ExtReal holds f ++ F = { (f + w) where w is Element of ExtREAL : w in F }