let X be non empty set ; :: thesis: 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 ) )
let f be PartFunc of X,ExtREAL ; :: thesis: for c being Real st f is nonnegative holds
( ( 0 <= c implies c (#) f is nonnegative ) & ( c <= 0 implies c (#) f is nonpositive ) )
let c be Real; :: thesis: ( f is nonnegative implies ( ( 0 <= c implies c (#) f is nonnegative ) & ( c <= 0 implies c (#) f is nonpositive ) ) )
assume A1: f is nonnegative ; :: thesis: ( ( 0 <= c implies c (#) f is nonnegative ) & ( c <= 0 implies c (#) f is nonpositive ) )

hereby :: thesis: ( c <= 0 implies c (#) f is nonpositive )

assume A2: 0 <= c ; :: thesis: c (#) f is nonnegative
set g = c (#) f;
for x being set st x in dom (c (#) f) holds
0 <= (c (#) f) . x

proof

let x be set ; :: thesis: ( x in dom (c (#) f) implies 0 <= (c (#) f) . x )
assume A3: x in dom (c (#) f) ; :: thesis: 0 <= (c (#) f) . x
0 <= f . x by A1, SUPINF_2:70;
then 0 <= (R_EAL c) * (f . x) by A2;
hence 0 <= (c (#) f) . x by A3, MESFUNC1:def 6; :: thesis: verum

end;

hence c (#) f is nonnegative by SUPINF_2:71; :: thesis: verum

end;

assume A4: c <= 0 ; :: thesis: c (#) f is nonpositive
set g = c (#) f;

now

let x be set ; :: thesis: ( x in dom (c (#) f) implies (c (#) f) . x <= 0 )
assume A5: x in dom (c (#) f) ; :: thesis: (c (#) f) . x <= 0
0 <= f . x by A1, SUPINF_2:70;
then (R_EAL c) * (f . x) <= 0 by A4;
hence (c (#) f) . x <= 0 by A5, MESFUNC1:def 6; :: thesis: verum

end;

hence c (#) f is nonpositive by Th15; :: thesis: verum