let x be object ; :: thesis: for Y being non empty set
for f being sequence of Y holds
( x in rng f iff ex n being Nat st x = f . n )
let Y be non empty set ; :: thesis: for f being sequence of Y holds
( x in rng f iff ex n being Nat st x = f . n )
let f be sequence of Y; :: thesis: ( x in rng f iff ex n being Nat st x = f . n )
thus ( x in rng f implies ex n being Nat st x = f . n ) :: thesis: ( ex n being Nat st x = f . n implies x in rng f )

proof

assume x in rng f ; :: thesis: ex n being Nat st x = f . n
then consider y being object such that
A1: y in dom f and
A2: x = f . y by FUNCT_1:def 3;
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 Nat such that A3: x = f . n ; :: thesis: x in rng f
A4: n in NAT by ORDINAL1:def 12;
dom f = NAT by FUNCT_2:def 1;
hence x in rng f by A3, FUNCT_1:def 3, A4; :: thesis: verum