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

proof

let x be set ; :: 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 consider y being set such that
W1: y in NAT and
W2: x = f . y by A3, FUNCT_1:def 5;
x is natural by W1, W2, A4;
hence x in NAT by ORDINAL1:def 13; :: thesis: verum

end;

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