theorem Th17: :: MESFUN6C:17

for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for c being Complex
for A being Element of S st f is A -measurable & A c= dom f holds
c (#) f is A -measurable