theorem Th46: :: PARTFUN2:46

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 holds
( ( c in dom f & d = f /. c ) iff [c,d] in f )