let seq be V113() sequence of NAT; :: thesis: for n being natural number holds n <= seq . n
let n be natural number ; :: thesis: n <= seq . n
a1: seq is Real_Sequence by FUNCT_2:7, NUMBERS:19;
rng seq c= NAT by RELAT_1:def 19;
hence n <= seq . n by a1, HEINE:2; :: thesis: verum