for x being object
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 )