theorem :: PARTFUN2:60

for C, D being non empty set
for c being Element of C
for d being Element of D
for f being PartFunc of C,D st f is one-to-one holds
( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )