theorem Th45: :: MEASURE9:47

for Y, S being non empty set
for F being PartFunc of Y,S
for M being Function of S,ExtREAL st M is V224() holds
M * F is nonnegative