let X be set ; :: thesis: for f being PartFunc of X,REAL st f is nonpositive holds
- f is nonnegative
let f be PartFunc of X,REAL; :: thesis: ( f is nonpositive implies - f is nonnegative )
assume A1: f is nonpositive ; :: thesis: - f is nonnegative

now :: thesis: for x being object st x in dom (- f) holds
0 <= (- f) . x

let x be object ; :: thesis: ( x in dom (- f) implies 0 <= (- f) . x )
assume x in dom (- f) ; :: thesis: 0 <= (- f) . x
then f . x <= 0 by A1, MESFUNC6:53;
then - (f . x) >= 0 ;
hence 0 <= (- f) . x by VALUED_1:8; :: thesis: verum

end;

hence - f is nonnegative by MESFUNC6:52; :: thesis: verum