let g, h be Function; :: thesis: ( ( not D is empty & dom g = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
g . <*x,y*> = f . (x,y) ) & dom h = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
h . <*x,y*> = f . (x,y) ) implies g = h ) & ( D is empty & g = {} & h = {} implies g = h ) )
thus ( not D is empty & dom g = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
g . <*x,y*> = f . (x,y) ) & dom h = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
h . <*x,y*> = f . (x,y) ) implies g = h ) :: thesis: ( D is empty & g = {} & h = {} implies g = h )

proof

assume that
A7: not D is empty and
A8: dom g = 2 -tuples_on D and
A9: for x, y being object st [x,y] in dom f holds
g . <*x,y*> = f . (x,y) and
A10: dom h = 2 -tuples_on D and
A11: for x, y being object st [x,y] in dom f holds
h . <*x,y*> = f . (x,y) ; :: thesis: g = h
thus dom g = dom h by A8, A10; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom g or g . b₁ = h . b₁ )
let a be object ; :: thesis: ( not a in dom g or g . a = h . a )
assume a in dom g ; :: thesis: g . a = h . a
then consider x, y being object such that
A12: ( x in D & y in D ) and
A13: a = <*x,y*> by A8, FINSEQ_2:137;
dom f = [:D,D:] by A7, FUNCT_2:def 1;
then A14: [x,y] in dom f by A12, ZFMISC_1:87;
hence g . a = f . (x,y) by A9, A13
.= h . a by A11, A13, A14 ;
:: thesis: verum

end;

thus ( D is empty & g = {} & h = {} implies g = h ) ; :: thesis: verum