let F be Function of NAT,ExtREAL; :: thesis: ( F is nonnegative implies for n, k being Element of NAT st n <= k holds
(Ser F) . n <= (Ser F) . k )
assume A1: F is nonnegative ; :: thesis: for n, k being Element of NAT st n <= k holds
(Ser F) . n <= (Ser F) . k
let n, k be Element of NAT ; :: thesis: ( n <= k implies (Ser F) . n <= (Ser F) . k )
defpred S₁[ Element of NAT ] means (Ser F) . n <= (Ser F) . (n + $1);
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: (Ser F) . n <= (Ser F) . (n + k) ; :: thesis: S₁[k + 1]
(Ser F) . (n + k) <= (Ser F) . ((n + k) + 1) by A1, SUPINF_2:40;
hence S₁[k + 1] by A3, XXREAL_0:2; :: thesis: verum

end;

assume n <= k ; :: thesis: (Ser F) . n <= (Ser F) . k
then consider s being Nat such that
A4: k = n + s by NAT_1:10;
reconsider s = s as Element of NAT by ORDINAL1:def 12;
A5: k = n + s by A4;
A6: S₁[ 0 ] ;
for s being Element of NAT holds S₁[s] from NAT_1:sch 1(A6, A2);
hence (Ser F) . n <= (Ser F) . k by A5; :: thesis: verum