let seq be V113() sequence of NAT; :: thesis: for n being Nat holds n <= seq . n
let n be Nat; :: 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