theorem :: MESFUNC6:55

for X being non empty set
for Y being set
for f being PartFunc of X,REAL st f is nonnegative holds
f | Y is nonnegative