let X be non empty set ; :: thesis: for Y being set
for f being PartFunc of X,ExtREAL st f is nonnegative holds
f | Y is nonnegative
let Y be set ; :: thesis: for f being PartFunc of X,ExtREAL st f is nonnegative holds
f | Y is nonnegative
let f be PartFunc of X,ExtREAL; :: thesis: ( f is nonnegative implies f | Y is nonnegative )
assume A1: f is nonnegative ; :: thesis: f | Y is nonnegative

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

let x be object ; :: thesis: ( x in dom (f | Y) implies 0 <= (f | Y) . x )
assume A2: x in dom (f | Y) ; :: thesis: 0 <= (f | Y) . x
then (f | Y) . x = f . x by FUNCT_1:47;
hence 0 <= (f | Y) . x by A1, A2, SUPINF_2:39; :: thesis: verum

end;

hence f | Y is nonnegative by SUPINF_2:52; :: thesis: verum