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

hereby :: thesis: ( ( for n being Element of X holds 0. <= F . n ) implies F is nonnegative )

assume F is nonnegative ; :: thesis: for n being Element of X holds 0. <= F . b₂
then A1: rng F is nonnegative ;
let n be Element of X; :: thesis: 0. <= F . b₁

per cases ( n in dom F or not n in dom F ) ;

suppose n in dom F ; :: thesis: 0. <= F . b₁

then F . n in rng F by FUNCT_1:def 3;
hence 0. <= F . n by A1; :: thesis: verum

end;

suppose not n in dom F ; :: thesis: 0. <= F . b₁

hence 0. <= F . n by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

assume A2: for n being Element of X holds 0. <= F . n ; :: thesis: F is nonnegative
let y be ExtReal; :: according to SUPINF_2:def 9,SUPINF_2:def 11 :: thesis: ( y in rng F implies 0. <= y )
assume y in rng F ; :: thesis: 0. <= y
then ex x being object st
( x in dom F & y = F . x ) by FUNCT_1:def 3;
hence 0. <= y by A2; :: thesis: verum