let Omega be non empty set ; :: thesis: for f being SetSequence of Omega
for x being set holds
( x in rng f iff ex n being Element of NAT st f . n = x )
let f be SetSequence of Omega; :: thesis: for x being set holds
( x in rng f iff ex n being Element of NAT st f . n = x )
let x be set ; :: thesis: ( x in rng f iff ex n being Element of NAT st f . n = x )

A1: now :: thesis: ( x in rng f implies ex n being Element of NAT st f . n = x )

assume x in rng f ; :: thesis: ex n being Element of NAT st f . n = x
then consider z being object such that
A2: z in dom f and
A3: x = f . z by FUNCT_1:def 3;
reconsider n = z as Element of NAT by A2, FUNCT_2:def 1;
take n = n; :: thesis: f . n = x
thus f . n = x by A3; :: thesis: verum

end;

dom f = NAT by FUNCT_2:def 1;
hence ( x in rng f iff ex n being Element of NAT st f . n = x ) by A1, FUNCT_1:def 3; :: thesis: verum