thus ( p is nonnegative implies for i being Nat st i in dom p holds
p . i >= 0 ) by FUNCT_1:3; :: thesis: ( ( for i being Nat st i in dom p holds
p . i >= 0 ) implies p is nonnegative )
assume A1: for i being Nat st i in dom p holds
p . i >= 0 ; :: thesis: p is nonnegative
let r be Real; :: according to PARTFUN3:def 4 :: thesis: ( not r in rng p or 0 <= r )
assume r in rng p ; :: thesis: 0 <= r
then ex j being Nat st
( j in dom p & r = p . j ) by FINSEQ_2:10;
hence 0 <= r by A1; :: thesis: verum