hereby :: thesis: ( ( for i being Element of NAT st i in dom p holds
p . i >= 0 ) implies p is nonnegative )

assume A1: p is nonnegative ; :: thesis: for i being Element of NAT st i in dom p holds
p . i >= 0
let i be Element of NAT ; :: thesis: ( i in dom p implies p . i >= 0 )
assume A2: i in dom p ; :: thesis: p . i >= 0
p . i in rng p by A2, FUNCT_1:12;
hence p . i >= 0 by A1, PARTFUN3:def 4; :: thesis: verum

end;

assume A3: for i being Element of NAT st i in dom p holds
p . i >= 0 ; :: thesis: p is nonnegative
let r be real number ; :: according to PARTFUN3:def 4 :: thesis: ( not r in rng p or 0 <= r )
assume r in rng p ; :: thesis: 0 <= r
then consider j being Nat such that
A4: ( j in dom p & r = p . j ) by FINSEQ_2:11;
thus 0 <= r by A3, A4; :: thesis: verum