let f1, f2 be Function; :: thesis: ( dom f1 = proj1 (dom f) & ( for x being object st x in proj1 (dom f) holds
ex g being Function st
( f1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g holds
g . y = f . (x,y) ) ) ) & dom f2 = proj1 (dom f) & ( for x being object st x in proj1 (dom f) holds
ex g being Function st
( f2 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g holds
g . y = f . (x,y) ) ) ) implies f1 = f2 )
assume that
A9: dom f1 = proj1 (dom f) and
A10: for x being object st x in proj1 (dom f) holds
ex g being Function st
( f1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g holds
g . y = f . (x,y) ) ) and
A11: dom f2 = proj1 (dom f) and
A12: for x being object st x in proj1 (dom f) holds
ex g being Function st
( f2 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g holds
g . y = f . (x,y) ) ) ; :: thesis: f1 = f2

now :: thesis: for x being object st x in proj1 (dom f) holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in proj1 (dom f) implies f1 . x = f2 . x )
assume A13: x in proj1 (dom f) ; :: thesis: f1 . x = f2 . x
then consider g1 being Function such that
A14: f1 . x = g1 and
A15: dom g1 = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) and
A16: for y being object st y in dom g1 holds
g1 . y = f . (x,y) by A10;
consider g2 being Function such that
A17: f2 . x = g2 and
A18: dom g2 = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) and
A19: for y being object st y in dom g2 holds
g2 . y = f . (x,y) by A12, A13;

now :: thesis: for y being object st y in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) holds
g1 . y = g2 . y

let y be object ; :: thesis: ( y in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) implies g1 . y = g2 . y )
assume A20: y in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) ; :: thesis: g1 . y = g2 . y
then g1 . y = f . (x,y) by A15, A16;
hence g1 . y = g2 . y by A18, A19, A20; :: thesis: verum

end;

hence f1 . x = f2 . x by A14, A15, A17, A18, FUNCT_1:2; :: thesis: verum

end;

hence f1 = f2 by A9, A11; :: thesis: verum