theorem Th52: :: MESFUNC6:52

for X being set
for f being PartFunc of X,REAL st ( for x being object st x in dom f holds
0 <= f . x ) holds
f is nonnegative