let n be Element of NAT ; :: thesis: for seq being Real_Sequence st seq is increasing & rng seq c= NAT holds
n <= seq . n
let seq be Real_Sequence; :: thesis: ( seq is increasing & rng seq c= NAT implies n <= seq . n )
defpred S₁[ Element of NAT ] means $1 <= seq . $1;
assume that
A1: seq is increasing and
A2: rng seq c= NAT ; :: thesis: n <= seq . n
0 in NAT ;
then 0 in dom seq by FUNCT_2:def 1;
then seq . 0 in rng seq by FUNCT_1:def 5;
then seq . 0 is natural by A2;
then A3: S₁[ 0 ] by NAT_1:2;
A4: 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 A5: k <= seq . k ; :: thesis: S₁[k + 1]
k + 1 in NAT ;
then k + 1 in dom seq by FUNCT_2:def 1;
then seq . (k + 1) in rng seq by FUNCT_1:def 5;
then reconsider k' = seq . (k + 1) as Element of NAT by A2;
seq . k < seq . (k + 1) by A1, SEQM_3:def 11;
then k < k' by A5, XXREAL_0:2;
hence S₁[k + 1] by NAT_1:13; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
hence n <= seq . n ; :: thesis: verum