theorem :: FUNCT_1:60

for x1, x2 being object
for f being Function st x1 in dom f & x2 in dom f holds
f .: {x1,x2} = {(f . x1),(f . x2)}