let X be non empty set ; :: thesis: 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 ) )

let f be PartFunc of X,ExtREAL; :: thesis: for c being Real st f is nonpositive holds
( ( 0 <= c implies c (#) f is nonpositive ) & ( c <= 0 implies c (#) f is nonnegative ) )

let c be Real; :: thesis: ( f is nonpositive implies ( ( 0 <= c implies c (#) f is nonpositive ) & ( c <= 0 implies c (#) f is nonnegative ) ) )
set g = c (#) f;
assume A1: f is nonpositive ; :: thesis: ( ( 0 <= c implies c (#) f is nonpositive ) & ( c <= 0 implies c (#) f is nonnegative ) )
hereby :: thesis: ( c <= 0 implies c (#) f is nonnegative )
set g = c (#) f;
assume A2: 0 <= c ; :: thesis: c (#) f is nonpositive
for x being set st x in dom (c (#) f) holds
(c (#) f) . x <= 0
proof
let x be set ; :: thesis: ( x in dom (c (#) f) implies (c (#) f) . x <= 0 )
f . x <= 0 by ;
then A3: c * (f . x) <= 0 by A2;
assume x in dom (c (#) f) ; :: thesis: (c (#) f) . x <= 0
hence (c (#) f) . x <= 0 by ; :: thesis: verum
end;
hence c (#) f is nonpositive by MESFUNC5:9; :: thesis: verum
end;
assume A4: c <= 0 ; :: thesis: c (#) f is nonnegative
now :: thesis: for x being object st x in dom (c (#) f) holds
0 <= (c (#) f) . x
let x be object ; :: thesis: ( x in dom (c (#) f) implies 0 <= (c (#) f) . x )
f . x <= 0 by ;
then A5: 0 <= c * (f . x) by A4;
assume x in dom (c (#) f) ; :: thesis: 0 <= (c (#) f) . x
hence 0 <= (c (#) f) . x by ; :: thesis: verum
end;
hence c (#) f is nonnegative by SUPINF_2:52; :: thesis: verum