theorem :: PARTFUN2:12

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