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

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

hence
f | Y is nonnegative
by SUPINF_2:52; :: thesis: verum0 <= (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;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