for X being set
for F being PartFunc of X,ExtREAL holds
( F is nonnegative iff for n being Element of X holds 0. <= F . n )