theorem Th4: :: MESFUN11:4

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