let D be Pos_Denum_Set_of_R_EAL; :: thesis: for N being Num of D
for n, m being Element of NAT holds (Ser (D,N)) . n <= (Ser (D,N)) . (n + m)
let N be Num of D; :: thesis: for n, m being Element of NAT holds (Ser (D,N)) . n <= (Ser (D,N)) . (n + m)
let n, m be Element of NAT ; :: thesis: (Ser (D,N)) . n <= (Ser (D,N)) . (n + m)
defpred S₁[ Element of NAT ] means (Ser (D,N)) . n <= (Ser (D,N)) . (n + $1);
A1: 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] )
(Ser (D,N)) . (n + (k + 1)) = (Ser (D,N)) . ((n + k) + 1) ;
then A2: (Ser (D,N)) . (n + k) <= (Ser (D,N)) . (n + (k + 1)) by Th55;
assume (Ser (D,N)) . n <= (Ser (D,N)) . (n + k) ; :: thesis: S₁[k + 1]
hence S₁[k + 1] by A2, XXREAL_0:2; :: thesis: verum

end;

A3: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A1);
hence (Ser (D,N)) . n <= (Ser (D,N)) . (n + m) ; :: thesis: verum