let D be Pos_Denum_Set_of_R_EAL; :: thesis: for N being Num of D
for n being Element of NAT holds
( (Ser (D,N)) . n <= (Ser (D,N)) . (n + 1) & 0. <= (Ser (D,N)) . n )
let N be Num of D; :: thesis: for n being Element of NAT holds
( (Ser (D,N)) . n <= (Ser (D,N)) . (n + 1) & 0. <= (Ser (D,N)) . n )
let n be Element of NAT ; :: thesis: ( (Ser (D,N)) . n <= (Ser (D,N)) . (n + 1) & 0. <= (Ser (D,N)) . n )
set F = Ser (D,N);
defpred S₁[ Element of NAT ] means ( (Ser (D,N)) . $1 <= (Ser (D,N)) . ($1 + 1) & 0. <= (Ser (D,N)) . $1 );
A1: (Ser (D,N)) . (0 + 1) = ((Ser (D,N)) . 0) + (N . 1) by Def17;
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 that
A3: (Ser (D,N)) . k <= (Ser (D,N)) . (k + 1) and
A4: 0. <= (Ser (D,N)) . k ; :: thesis: S₁[k + 1]
A5: 0. <= N . ((k + 1) + 1) by Th54;
(Ser (D,N)) . ((k + 1) + 1) = ((Ser (D,N)) . (k + 1)) + (N . ((k + 1) + 1)) by Def17;
hence S₁[k + 1] by A3, A4, A5, XXREAL_0:2, XXREAL_3:39; :: thesis: verum

end;

(Ser (D,N)) . 0 = N . 0 by Def17;
then A6: S₁[ 0 ] by A1, Th54, XXREAL_3:39;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A2);
hence ( (Ser (D,N)) . n <= (Ser (D,N)) . (n + 1) & 0. <= (Ser (D,N)) . n ) ; :: thesis: verum