let F be Function of NAT ,ExtREAL ; :: thesis: for n being Element of NAT st F is nonnegative holds
( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n )
let n be Element of NAT ; :: thesis: ( F is nonnegative implies ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) )
reconsider N = F as Num of rng F by Def16;
assume F is nonnegative ; :: thesis: ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n )
then A1: rng F is Pos_Denum_Set_of_R_EAL by Def22;
Ser F = Ser (rng F),N by Def21;
hence ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) by A1, Th55; :: thesis: verum