theorem :: PARTFUN2:13

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