A1: <*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 A2: i in dom <*1*> ; :: thesis: <*1*> . i >= 0
i in Seg 1 by A2, FINSEQ_1:def 8;
then ( i >= 1 & i <= 1 ) by FINSEQ_1:3;
then i = 1 by XXREAL_0:1;
hence <*1*> . i >= 0 by FINSEQ_1:57; :: thesis: verum

end;

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

end;

take <*1*> ; :: thesis: <*1*> is nonnegative
thus <*1*> is nonnegative by A1; :: thesis: verum