defpred S₁[ Nat] means (Ser F) . (n + $1) <= (Ser F) . n;
let r be Element of NAT ; :: thesis:
assume n <= r ; :: thesis:
then A4: ex m being Nat st r = n + m by NAT_1:10;
A5: for s being Nat st S₁[s] holds
S₁[s + 1]

let s be Nat; :: thesis:
reconsider s9 = s as Element of NAT by ORDINAL1:def 12;
reconsider y = (Ser F) . (n + s) as R_eal ;
n9 + (s9 + 1) = (n9 + s9) + 1 ;
then A6: (Ser F) . (n9 + (s9 + 1)) = y + (F . (n9 + (s9 + 1))) by Def11;
n + 0 <= n + (s + 1) by XREAL_1:7;
then A7: F . (n9 + (s9 + 1)) = 0. by A2;
assume (Ser F) . (n + s) <= (Ser F) . n ; :: thesis:
hence S₁[s + 1] by A6, A7, XXREAL_3:4; :: thesis:

end;

A8: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A8, A5);
hence (Ser F) . r <= (Ser F) . n by A4; :: thesis:

end;

let r be Element of NAT ; :: thesis:
assume r <= n ; :: thesis:
then consider m being Nat such that
A10: n = r + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
thus (Ser F) . r <= (Ser F) . n by A1, Th40, A10; :: thesis:

end;

let y be ExtReal; :: thesis:
A11: dom (Ser F) = NAT by FUNCT_2:def 1;
assume y in rng (Ser F) ; :: thesis:
then consider m being object such that
A12: m in NAT and
A13: y = (Ser F) . m by A11, FUNCT_1:def 3;
reconsider m = m as Element of NAT by A12;
( m <= n or n <= m ) ;
hence y <= (Ser F) . n by A3, A9, A13; :: thesis:

end;