let f1, f2 be Function; :: thesis: ( dom f1 = proj1 (dom f) & ( for x being set 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 set st y in dom g holds
g . y = f . x,y ) ) ) & dom f2 = proj1 (dom f) & ( for x being set 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 set st y in dom g holds
g . y = f . x,y ) ) ) implies f1 = f2 )
assume that
A6: ( dom f1 = proj1 (dom f) & ( for x being set 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 set st y in dom g holds
g . y = f . x,y ) ) ) ) and
A7: ( dom f2 = proj1 (dom f) & ( for x being set 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 set st y in dom g holds
g . y = f . x,y ) ) ) ) ; :: thesis: f1 = f2

now

let x be set ; :: thesis: ( x in proj1 (dom f) implies f1 . x = f2 . x )
assume A8: x in proj1 (dom f) ; :: thesis: f1 . x = f2 . x
then consider g1 being Function such that
A9: ( f1 . x = g1 & dom g1 = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g1 holds
g1 . y = f . x,y ) ) by A6;
consider g2 being Function such that
A10: ( f2 . x = g2 & dom g2 = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g2 holds
g2 . y = f . x,y ) ) by A7, A8;

now

let y be set ; :: thesis: ( y in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) implies g1 . y = g2 . y )
assume y in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) ; :: thesis: g1 . y = g2 . y
then ( g1 . y = f . x,y & g2 . y = f . x,y ) by A9, A10;
hence g1 . y = g2 . y ; :: thesis: verum

end;

hence f1 . x = f2 . x by A9, A10, FUNCT_1:9; :: thesis: verum

end;

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