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

now :: thesis: for x, y being object holds
( ( [x,y] in g implies ( x in X & [x,y] in f ) ) & ( x in X & [x,y] in f implies [x,y] in g ) )

let x, y be object ; :: 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 A3: [x,y] in g ; :: thesis: ( x in X & [x,y] in f )
then A4: x in dom g by XTUPLE_0:def 12;
hence x in X by A1, XBOOLE_0:def 4; :: thesis: [x,y] in f
A5: x in dom f by A1, A4, XBOOLE_0:def 4;
reconsider yy = y as set by TARSKI:1;
yy = g . x by A3, A4, Def2
.= f . x by A2, A4 ;
hence [x,y] in f by A5, Def2; :: thesis: verum

end;

assume A6: x in X ; :: thesis: ( [x,y] in f implies [x,y] in g )
assume A7: [x,y] in f ; :: thesis: [x,y] in g
then A8: x in dom f by XTUPLE_0:def 12;
then A9: x in dom g by A1, A6, XBOOLE_0:def 4;
reconsider yy = y as set by TARSKI:1;
yy = f . x by A7, A8, Def2
.= g . x by A2, A9 ;
hence [x,y] in g by A9, Def2; :: thesis: verum

end;

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