take <*1*> ; :: thesis: <*1*> is nonnegative
<*1*> is nonnegative

proof

set p = <*1*>;
for i being Element of NAT st i in dom <*1*> holds
<*1*> . i >= 0

proof

let i be Element of NAT ; :: thesis: ( i in dom <*1*> implies <*1*> . i >= 0 )
assume i in dom <*1*> ; :: thesis: <*1*> . i >= 0
then A1: i in Seg 1 by FINSEQ_1:def 8;
then A2: i <= 1 by FINSEQ_1:1;
i >= 1 by A1, FINSEQ_1:1;
then i = 1 by A2, XXREAL_0:1;
hence <*1*> . i >= 0 by FINSEQ_1:40; :: thesis: verum

end;

hence <*1*> is nonnegative by Def1; :: thesis: verum

end;

hence <*1*> is nonnegative ; :: thesis: verum