let seq be Real_Sequence; :: thesis: ( seq is sequence of NAT iff for n being Nat holds seq . n is Element of NAT )
thus ( seq is sequence of NAT implies for n being Nat holds seq . n is Element of NAT ) by ORDINAL1:def 12; :: thesis: ( ( for n being Nat holds seq . n is Element of NAT ) implies seq is sequence of NAT )
assume A1: for n being Nat holds seq . n is Element of NAT ; :: thesis: seq is sequence of NAT
rng seq c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng seq or x in NAT )
assume x in rng seq ; :: thesis: x in NAT
then consider y being object such that
A2: y in dom seq and
A3: x = seq . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A2, FUNCT_2:def 1;
x = seq . y by A3;
then x is Element of NAT by A1;
hence x in NAT ; :: thesis: verum

end;

hence seq is sequence of NAT by FUNCT_2:6; :: thesis: verum