theorem Th9: :: MESFUN11:9

for X being non empty set
for f, g being PartFunc of X,ExtREAL
for a being ExtReal
for r being Real st r <> 0 & g = r (#) f holds
eq_dom (f,a) = eq_dom (g,(a * r))