theorem Th2: :: MESFUN11:2

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