theorem Th11: :: PARTFUN2:11

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