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 H1( Nat) -> Element of omega = $1 + n0;
consider NS being Real_Sequence such that
A1: for n being Nat holds NS . n = H1(n) from SEQ_1:sch 1();
 A2: NS is increasing
proof
let n be Nat; :: according to SEQM_3:def 6 :: thesis: not NS . (n + 1) <= NS . n
n < n + 1 by NAT_1:13;
then n + n0 < (n + 1) + n0 by XREAL_1:6;
then NS . n < (n + 1) + n0 by A1;
hence not NS . (n + 1) <= NS . n by A1; :: thesis: verum
end;
for n being Nat holds NS . n is Element of NAT
proof
let n be 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:13;
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