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

let x be set ; :: 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:70;
hence 0 <= (f | Y) . x by A1, A2, SUPINF_2:58; :: thesis: verum

end;

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