let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for r being Real st f is nonnegative holds
( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) )
let f be PartFunc of X,REAL; :: thesis: for r being Real st f is nonnegative holds
( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) )
let r be Real; :: thesis: ( f is nonnegative implies ( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) ) )
assume A1: f is nonnegative ; :: thesis: ( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) )
hereby :: thesis: ( r <= 0 implies r (#) f is nonpositive )
assume A2: 0 <= r ; :: thesis: r (#) f is nonnegative
now :: thesis: for x being object st x in dom (r (#) f) holds
0 <= (r (#) f) . x
let x be object ; :: thesis: ( x in dom (r (#) f) implies 0 <= (r (#) f) . x )
assume A3: x in dom (r (#) f) ; :: thesis: 0 <= (r (#) f) . x
0 <= f . x by A1, Th51;
then 0 * r <= r * (f . x) by A2;
hence 0 <= (r (#) f) . x by A3, VALUED_1:def 5; :: thesis: verum
end;
hence r (#) f is nonnegative by Th52; :: thesis: verum
end;
assume A4: r <= 0 ; :: thesis: r (#) f is nonpositive
now :: thesis: for x being object st x in dom (r (#) f) holds
(r (#) f) . x <= 0
let x be object ; :: thesis: ( x in dom (r (#) f) implies (r (#) f) . x <= 0 )
assume A5: x in dom (r (#) f) ; :: thesis: (r (#) f) . x <= 0
0 <= f . x by A1, Th51;
then r * (f . x) <= r * 0 by A4;
hence (r (#) f) . x <= 0 by A5, VALUED_1:def 5; :: thesis: verum
end;
hence r (#) f is nonpositive by Th54; :: thesis: verum