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

now :: thesis: for r being R_eal st r in rng (f | A) holds
r <= 0

let r be R_eal; :: thesis: ( r in rng (f | A) implies r <= 0 )
assume r in rng (f | A) ; :: thesis: r <= 0
then consider x being object such that
A2: ( x in dom (f | A) & r = (f | A) . x ) by FUNCT_1:def 3;
f . x <= 0 by A1, A2, MESFUNC6:53;
hence r <= 0 by A2, FUNCT_1:47; :: thesis: verum

end;

hence f | A is nonpositive by MESFUNC5:def 1, MESFUNC5:def 2; :: thesis: verum