theorem :: PARTFUN2:25

for C, D being non empty set
for c1, c2 being Element of C
for f being PartFunc of C,D st c1 in dom f & c2 in dom f holds
f .: {c1,c2} = {(f /. c1),(f /. c2)}