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 object 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 object 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 object st [x,y] in dom f1 holds
f1 . (x,y) = f2 . (x,y) ; :: thesis: f1 = f2
for z being object st z in dom f1 holds
f1 . z = f2 . z
proof
let z be object ; :: 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 object 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; :: thesis: verum