let X, Y, Z be set ; :: thesis: for f1, f2 being PartFunc of [:X,Y:],Z st dom f1 = dom f2 & ( for x, y being set st [x,y] in dom f1 holds
f1 . x,y = f2 . x,y ) holds
f1 = f2
let f1, f2 be PartFunc of [:X,Y:],Z; :: thesis: ( dom f1 = dom f2 & ( for x, y being set st [x,y] in dom f1 holds
f1 . x,y = f2 . x,y ) implies f1 = f2 )
assume that
A1: dom f1 = dom f2 and
A2: for x, y being set st [x,y] in dom f1 holds
f1 . x,y = f2 . x,y ; :: thesis: f1 = f2
for z being set st z in dom f1 holds
f1 . z = f2 . z

proof

let z be set ; :: thesis: ( z in dom f1 implies f1 . z = f2 . z )
assume A3: z in dom f1 ; :: thesis: f1 . z = f2 . z
then consider x, y being set such that
A4: z = [x,y] by RELAT_1:def 1;
f1 . x,y = f2 . x,y by A2, A3, A4;
hence f1 . z = f2 . z by A4; :: thesis: verum

end;

hence f1 = f2 by A1, FUNCT_1:9; :: thesis: verum