let f be Function; :: thesis: ( f is sequence of NAT iff ( dom f = NAT & ( for x being object st x in NAT holds
f . x is natural ) ) )
thus ( f is sequence of NAT implies ( dom f = NAT & ( for x being object st x in NAT holds
f . x is natural ) ) ) by FUNCT_2:def 1; :: thesis: ( dom f = NAT & ( for x being object st x in NAT holds
f . x is natural ) implies f is sequence of NAT )
assume that
A1: dom f = NAT and
A2: for x being object st x in NAT holds
f . x is natural ; :: thesis: f is sequence of NAT
rng f c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in NAT )
assume x in rng f ; :: thesis: x in NAT
then ex y being object st
( y in NAT & x = f . y ) by A1, FUNCT_1:def 3;
then x is natural by A2;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

hence f is sequence of NAT by A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum