let x be set ; :: thesis: for Y being non empty set
for f being Function of NAT ,Y holds
( x in rng f iff ex n being Element of NAT st x = f . n )
let Y be non empty set ; :: thesis: for f being Function of NAT ,Y holds
( x in rng f iff ex n being Element of NAT st x = f . n )
let f be Function of NAT ,Y; :: thesis: ( x in rng f iff ex n being Element of NAT st x = f . n )
thus ( x in rng f implies ex n being Element of NAT st x = f . n ) :: thesis: ( ex n being Element of NAT st x = f . n implies x in rng f )

proof

assume x in rng f ; :: thesis: ex n being Element of NAT st x = f . n
then consider y being set such that
A1: y in dom f and
A2: x = f . y by FUNCT_1:def 5;
reconsider m = y as Element of NAT by A1;
take m ; :: thesis: x = f . m
thus x = f . m by A2; :: thesis: verum

end;

given n being Element of NAT such that A3: x = f . n ; :: thesis: x in rng f
dom f = NAT by FUNCT_2:def 1;
hence x in rng f by A3, FUNCT_1:def 5; :: thesis: verum