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 ) )
assume A1: F is nonnegative ; :: thesis: ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n )
reconsider N = F as Num of rng F by Def16;
A2: Ser F = Ser (rng F),N by Def21;
rng F is Pos_Denum_Set_of_R_EAL by A1, Def22;
hence ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) by A2, Th55; :: thesis: verum