let n0 be Element of NAT ; :: thesis: ex NS being increasing sequence of NAT st
for n being Element of NAT holds NS . n = n + n0
deffunc H₁( Element of NAT ) -> Element of NAT = $1 + n0;
consider NS being Real_Sequence such that
A1: for n being Element of NAT holds NS . n = H₁(n) from SEQ_1:sch 1();
A2: NS is increasing

proof

let n be Element of NAT ; :: according to SEQM_3:def 11 :: thesis: not NS . (n + 1) <= NS . n
n < n + 1 by NAT_1:13;
then n + n0 < (n + 1) + n0 by XREAL_1:8;
then NS . n < (n + 1) + n0 by A1;
hence not NS . (n + 1) <= NS . n by A1; :: thesis: verum

end;

for n being Element of NAT holds NS . n is Element of NAT

proof

let n be Element of NAT ; :: thesis: NS . n is Element of NAT
n + n0 in NAT ;
hence NS . n is Element of NAT by A1; :: thesis: verum

end;

then reconsider NS = NS as increasing sequence of NAT by A2, SEQM_3:29;
take NS ; :: thesis: for n being Element of NAT holds NS . n = n + n0
thus for n being Element of NAT holds NS . n = n + n0 by A1; :: thesis: verum