for y being object
for X, Y being set
for f being PartFunc of X,Y st y in rng f holds
ex x being Element of X st
( x in dom f & y = f . x )