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