theorem :: SEQM_3:13

for seq being Real_Sequence holds
( seq is sequence of NAT iff for n being Nat holds seq . n is Element of NAT )