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

proof

assume that
not f is empty and
A5: dom g = 1 -tuples_on (dom f) and
A6: for x being object st x in dom f holds
g . <*x*> = f . x and
A7: dom h = 1 -tuples_on (dom f) and
A8: for x being object st x in dom f holds
h . <*x*> = f . x ; :: thesis: g = h
thus dom g = dom h by A5, A7; :: 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 being set such that
A9: ( x in dom f & a = <*x*> ) by A5, FINSEQ_2:135;
thus g . a = f . x by A6, A9
.= h . a by A8, A9 ; :: thesis: verum

end;

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