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 ;

now :: thesis: for y being ExtReal st y in rng (f | Y) holds
0. <= y

let y be ExtReal; :: thesis: ( y in rng (f | Y) implies 0. <= y )
assume y in rng (f | Y) ; :: thesis: 0. <= y
then consider x being object such that
A2: x in dom (f | Y) and
A3: (f | Y) . x = y by FUNCT_1:def 3;
x in (dom f) /\ Y by A2, RELAT_1:61;
then A4: x in dom f by XBOOLE_0:def 4;
(f | Y) . x = f . x by A2, FUNCT_1:47;
then (f | Y) . x in rng f by A4, FUNCT_1:3;
hence 0. <= y by A1, A3; :: thesis: verum

end;

then rng (f | Y) is nonnegative ;
hence f | Y is nonnegative ; :: thesis: verum