let F be sequence of ExtREAL; :: thesis: ( F is nonnegative implies for n being Nat holds F . n <= (Ser F) . n )
assume A1: F is nonnegative ; :: thesis: for n being Nat holds F . n <= (Ser F) . n
let n be Nat; :: thesis: F . n <= (Ser F) . n

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: F . n <= (Ser F) . n

hence F . n <= (Ser F) . n by SUPINF_2:def 11; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: F . n <= (Ser F) . n

then consider k being Nat such that
A2: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A3: 0. <= (Ser F) . k by A1, SUPINF_2:40;
(Ser F) . n = ((Ser F) . k) + (F . n) by A2, SUPINF_2:def 11;
then 0. + (F . n) <= (Ser F) . n by A3, XXREAL_3:36;
hence F . n <= (Ser F) . n by XXREAL_3:4; :: thesis: verum

end;

end;