set F = <*+infty*>;

now :: thesis: for i being object holds <*+infty*> . i >= 0

let i be object ; :: thesis: <*+infty*> . b₁ >= 0

per cases ( i in dom <*+infty*> or not i in dom <*+infty*> ) ;

suppose i in dom <*+infty*> ; :: thesis: <*+infty*> . b₁ >= 0

then i in Seg 1 by FINSEQ_1:38;
then i = 1 by TARSKI:def 1, FINSEQ_1:2;
hence <*+infty*> . i >= 0 by FINSEQ_1:40; :: thesis: verum

end;

suppose not i in dom <*+infty*> ; :: thesis: <*+infty*> . b₁ >= 0

hence <*+infty*> . i >= 0 by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence <*+infty*> is nonnegative by SUPINF_2:51; :: thesis: <*+infty*> is V251()
hence <*+infty*> is V251() ; :: thesis: verum