let X be set ; :: thesis: for F being PartFunc of X,ExtREAL st ( for n being object st n in dom F holds

0. <= F . n ) holds

F is nonnegative

let F be PartFunc of X,ExtREAL; :: thesis: ( ( for n being object st n in dom F holds

0. <= F . n ) implies F is nonnegative )

assume A1: for n being object st n in dom F 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 A1; :: thesis: verum

0. <= F . n ) holds

F is nonnegative

let F be PartFunc of X,ExtREAL; :: thesis: ( ( for n being object st n in dom F holds

0. <= F . n ) implies F is nonnegative )

assume A1: for n being object st n in dom F 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 A1; :: thesis: verum