theorem Th20: :: MESFUNC5:20

for X being non empty set
for f being PartFunc of X,ExtREAL
for c being Real st f is nonnegative holds
( ( 0 <= c implies c (#) f is nonnegative ) & ( c <= 0 implies c (#) f is nonpositive ) )