let X be set ; :: thesis: for F being PartFunc of X,ExtREAL st ( for n being set st n in dom F holds
0. <= F . n ) holds
F is nonnegative
let F be PartFunc of X,ExtREAL ; :: thesis: ( ( for n being set st n in dom F holds
0. <= F . n ) implies F is nonnegative )
assume A1: for n being set st n in dom F holds
0. <= F . n ; :: thesis: F is nonnegative
let y be R_eal; :: according to SUPINF_2:def 15,SUPINF_2:def 22 :: thesis: ( y in rng F implies 0. <= y )
assume y in rng F ; :: thesis: 0. <= y
then consider x being set such that
A2: x in dom F and
A3: y = F . x by FUNCT_1:def 5;
thus 0. <= y by A1, A2, A3; :: thesis: verum