let X be set ; :: thesis: for g, f being Function st dom g = (dom f) /\ X & ( for x being set st x in dom g holds
g . x = f . x ) holds
g = f | X
let g, f be Function; :: thesis: ( dom g = (dom f) /\ X & ( for x being set st x in dom g holds
g . x = f . x ) implies g = f | X )
assume that
A6: dom g = (dom f) /\ X and
A7: for x being set st x in dom g holds
g . x = f . x ; :: thesis: g = f | X

now

let x, y be set ; :: thesis: ( ( [x,y] in g implies ( x in X & [x,y] in f ) ) & ( x in X & [x,y] in f implies [x,y] in g ) )

hereby :: thesis: ( x in X & [x,y] in f implies [x,y] in g )

assume A8: [x,y] in g ; :: thesis: ( x in X & [x,y] in f )
then A9: x in dom g by RELAT_1:def 4;
hence x in X by A6, XBOOLE_0:def 4; :: thesis: [x,y] in f
A10: x in dom f by A6, A9, XBOOLE_0:def 4;
y = g . x by A8, A9, Def4
.= f . x by A7, A9 ;
hence [x,y] in f by A10, Def4; :: thesis: verum

end;

assume A11: x in X ; :: thesis: ( [x,y] in f implies [x,y] in g )
assume A12: [x,y] in f ; :: thesis: [x,y] in g
then A13: x in dom f by RELAT_1:def 4;
then A14: x in dom g by A6, A11, XBOOLE_0:def 4;
y = f . x by A12, A13, Def4
.= g . x by A7, A14 ;
hence [x,y] in g by A14, Def4; :: thesis: verum

end;

hence g = f | X by RELAT_1:def 11; :: thesis: verum