let Y be set ; :: thesis: for f, g being Function holds
( g = Y |` f iff ( ( for x being object holds
( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being object st x in dom g holds
g . x = f . x ) ) )
let f, g be Function; :: thesis: ( g = Y |` f iff ( ( for x being object holds
( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being object st x in dom g holds
g . x = f . x ) ) )

hereby :: thesis: ( ( for x being object holds
( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being object st x in dom g holds
g . x = f . x ) implies g = Y |` f )

assume A1: g = Y |` f ; :: thesis: ( ( for x being object holds
( ( x in dom g implies ( x in dom f & f . x in Y ) ) & ( x in dom f & f . x in Y implies x in dom g ) ) ) & ( for x being object st x in dom g holds
f . x = g . x ) )

hereby :: thesis: for x being object st x in dom g holds
f . x = g . x

let x be object ; :: thesis: ( ( x in dom g implies ( x in dom f & f . x in Y ) ) & ( x in dom f & f . x in Y implies x in dom g ) )

hereby :: thesis: ( x in dom f & f . x in Y implies x in dom g )

assume x in dom g ; :: thesis: ( x in dom f & f . x in Y )
then A2: [x,(g . x)] in g by Def2;
then A3: [x,(g . x)] in f by A1, RELAT_1:def 12;
hence x in dom f by XTUPLE_0:def 12; :: thesis: f . x in Y
then f . x = g . x by A3, Def2;
hence f . x in Y by A1, A2, RELAT_1:def 12; :: thesis: verum

end;

assume x in dom f ; :: thesis: ( f . x in Y implies x in dom g )
then A4: [x,(f . x)] in f by Def2;
assume f . x in Y ; :: thesis: x in dom g
then [x,(f . x)] in g by A1, A4, RELAT_1:def 12;
hence x in dom g by XTUPLE_0:def 12; :: thesis: verum

end;

let x be object ; :: thesis: ( x in dom g implies f . x = g . x )
assume x in dom g ; :: thesis: f . x = g . x
then [x,(g . x)] in g by Def2;
then A5: [x,(g . x)] in f by A1, RELAT_1:def 12;
then x in dom f by XTUPLE_0:def 12;
hence f . x = g . x by A5, Def2; :: thesis: verum

end;

assume that
A6: for x being object holds
( x in dom g iff ( x in dom f & f . x in Y ) ) and
A7: for x being object st x in dom g holds
g . x = f . x ; :: thesis: g = Y |` f

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

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

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

assume A8: [x,y] in g ; :: thesis: ( y in Y & [x,y] in f )
then A9: x in dom g by XTUPLE_0:def 12;
reconsider yy = y as set by TARSKI:1;
A10: yy = g . x by A8, Def2, A9
.= f . x by A7, A9 ;
hence y in Y by A6, A9; :: thesis: [x,y] in f
x in dom f by A6, A9;
hence [x,y] in f by A10, Def2; :: thesis: verum

end;

assume A11: y in Y ; :: thesis: ( [x,y] in f implies [x,y] in g )
assume A12: [x,y] in f ; :: thesis: [x,y] in g
then A13: y = f . x by Th1;
x in dom f by A12, XTUPLE_0:def 12;
then A14: x in dom g by A6, A11, A13;
then y = g . x by A7, A13;
hence [x,y] in g by A14, Def2; :: thesis: verum

end;

hence g = Y |` f by RELAT_1:def 12; :: thesis: verum