theorem Th2: :: MESFUNC7:2

for X being non empty set
for Y being set
for f being PartFunc of X,ExtREAL
for r being Real holds (r (#) f) | Y = r (#) (f | Y)