theorem :: FUNCT_4:66

for a, b, c, d being object
for g being Function st dom g = {a,b} & g . a = c & g . b = d holds
g = (a,b) --> (c,d)