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 ) ) )

set g = c (#) f;

assume A1: f is nonnegative ; :: thesis: ( ( 0 <= c implies c (#) f is nonnegative ) & ( c <= 0 implies c (#) f is nonpositive ) )

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 ) ) )

set g = c (#) f;

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 A4:
c <= 0
; :: thesis: c (#) f is nonpositive set g = c (#) f;

assume A2: 0 <= c ; :: thesis: c (#) f is nonnegative

for x being object st x in dom (c (#) f) holds

0 <= (c (#) f) . x

end;assume A2: 0 <= c ; :: thesis: c (#) f is nonnegative

for x being object st x in dom (c (#) f) holds

0 <= (c (#) f) . x

proof

hence
c (#) f is nonnegative
by SUPINF_2:52; :: thesis: verum
let x be object ; :: thesis: ( x in dom (c (#) f) implies 0 <= (c (#) f) . x )

0 <= f . x by A1, SUPINF_2:51;

then A3: 0 <= c * (f . x) by A2;

assume x in dom (c (#) f) ; :: thesis: 0 <= (c (#) f) . x

hence 0 <= (c (#) f) . x by A3, MESFUNC1:def 6; :: thesis: verum

end;0 <= f . x by A1, SUPINF_2:51;

then A3: 0 <= c * (f . x) by A2;

assume x in dom (c (#) f) ; :: thesis: 0 <= (c (#) f) . x

hence 0 <= (c (#) f) . x by A3, MESFUNC1:def 6; :: thesis: verum

now :: thesis: for x being set st x in dom (c (#) f) holds

(c (#) f) . x <= 0

hence
c (#) f is nonpositive
by Th9; :: thesis: verum(c (#) f) . x <= 0

let x be set ; :: thesis: ( x in dom (c (#) f) implies (c (#) f) . x <= 0 )

0 <= f . x by A1, SUPINF_2:51;

then A5: c * (f . x) <= 0 by A4;

assume x in dom (c (#) f) ; :: thesis: (c (#) f) . x <= 0

hence (c (#) f) . x <= 0 by A5, MESFUNC1:def 6; :: thesis: verum

end;0 <= f . x by A1, SUPINF_2:51;

then A5: c * (f . x) <= 0 by A4;

assume x in dom (c (#) f) ; :: thesis: (c (#) f) . x <= 0

hence (c (#) f) . x <= 0 by A5, MESFUNC1:def 6; :: thesis: verum