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_measurable_on A & A c= dom f holds
c (#) f is_measurable_on A