let X be non empty set ; :: thesis: for Y being set
for f being PartFunc of X,REAL st f is nonnegative holds
f | Y is nonnegative
let Y be set ; :: thesis: for f being PartFunc of X,REAL st f is nonnegative holds
f | Y is nonnegative
let f be PartFunc of X,REAL ; :: thesis: ( f is nonnegative implies f | Y is nonnegative )
assume f is nonnegative ; :: thesis: f | Y is nonnegative
then A1: rng f is nonnegative by SUPINF_2:def 22;

now

let y be R_eal; :: thesis: ( y in rng (f | Y) implies 0. <= y )
assume y in rng (f | Y) ; :: thesis: 0. <= y
then consider x being set such that
A2: ( x in dom (f | Y) & (f | Y) . x = y ) by FUNCT_1:def 5;
x in (dom f) /\ Y by A2, RELAT_1:90;
then ( x in dom f & (f | Y) . x = f . x ) by A2, FUNCT_1:70, XBOOLE_0:def 4;
then (f | Y) . x in rng f by FUNCT_1:12;
hence 0. <= y by A1, A2, SUPINF_2:def 15; :: thesis: verum

end;

then rng (f | Y) is nonnegative by SUPINF_2:def 15;
hence f | Y is nonnegative by SUPINF_2:def 22; :: thesis: verum