let Y be non empty set ; :: thesis: for f being Function of NAT ,Y holds rng f = { (f . k) where k is Element of NAT : 0 <= k }
let f be Function of NAT ,Y; :: thesis: rng f = { (f . k) where k is Element of NAT : 0 <= k }
B: dom f = NAT by FUNCT_2:def 1;
set Z = { (f . k) where k is Element of NAT : 0 <= k } ;
A00: { (f . k) where k is Element of NAT : 0 <= k } c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . k) where k is Element of NAT : 0 <= k } or x in rng f )
assume x in { (f . k) where k is Element of NAT : 0 <= k } ; :: thesis: x in rng f
then consider n1 being Element of NAT such that
AA0: ( x = f . n1 & 0 <= n1 ) ;
thus x in rng f by AA0, FUNCT_2:6; :: thesis: verum

end;

rng f c= { (f . k) where k is Element of NAT : 0 <= k }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in { (f . k) where k is Element of NAT : 0 <= k } )
assume y in rng f ; :: thesis: y in { (f . k) where k is Element of NAT : 0 <= k }
then consider n being set such that
AB: ( n in NAT & y = f . n ) by B, FUNCT_1:def 5;
reconsider n = n as Element of NAT by AB;
0 <= n by NAT_1:2;
hence y in { (f . k) where k is Element of NAT : 0 <= k } by AB; :: thesis: verum

end;

hence rng f = { (f . k) where k is Element of NAT : 0 <= k } by A00, XBOOLE_0:def 10; :: thesis: verum