theorem Th6: :: FUNCT_3:6

for X, Y being set
for f, g being Function st dom f = [:X,Y:] & dom g = [:X,Y:] & ( for x, y being object st x in X & y in Y holds
f . (x,y) = g . (x,y) ) holds
f = g