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) and
A3: (f | Y) . x = y by FUNCT_1:def 5;
x in (dom f) /\ Y by A2, RELAT_1:90;
then A4: x in dom f by XBOOLE_0:def 4;
(f | Y) . x = f . x by A2, FUNCT_1:70;
then (f | Y) . x in rng f by A4, FUNCT_1:12;
hence 0. <= y by A1, A3, 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