let seq be Real_Sequence; :: thesis: ( seq is sequence of NAT iff for n being Element of NAT holds seq . n is Element of NAT )
thus ( seq is sequence of NAT implies for n being Element of NAT holds seq . n is Element of NAT ) :: thesis: ( ( for n being Element of NAT holds seq . n is Element of NAT ) implies seq is sequence of NAT )

proof

assume seq is sequence of NAT ; :: thesis: for n being Element of NAT holds seq . n is Element of NAT
then A1: rng seq c= NAT by VALUED_0:def 6;
let n be Element of NAT ; :: thesis: seq . n is Element of NAT
n in NAT ;
then n in dom seq by FUNCT_2:def 1;
then seq . n in rng seq by FUNCT_1:def 3;
hence seq . n is Element of NAT by A1; :: thesis: verum

end;

assume A2: for n being Element of NAT holds seq . n is Element of NAT ; :: thesis: seq is sequence of NAT
rng seq c= NAT

proof

let x be set ; :: 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 set such that
A3: y in dom seq and
A4: x = seq . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A3, FUNCT_2:def 1;
x = seq . y by A4;
then x is Element of NAT by A2;
hence x in NAT ; :: thesis: verum

end;

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