theorem :: REAL_3:10

for f being Function holds
( f is sequence of NAT iff ( dom f = NAT & ( for x being object st x in NAT holds
f . x is natural ) ) )