let Y be set ; :: thesis:
let f, g be Function; :: thesis:

hereby :: thesis:

assume A1: g = Y |` f ; :: thesis:

hereby :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in dom g ; :: thesis:
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:
then f . x = g . x by A3, Def2;
hence f . x in Y by A1, A2, RELAT_1:def 12; :: thesis:

end;

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

end;

let x be object ; :: thesis:
assume x in dom g ; :: thesis:
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:

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:

let x, y be object ; :: thesis:

hereby :: thesis:

assume A8: [x,y] in g ; :: thesis:
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 in dom f by A6, A9;
hence [x,y] in f by A10, Def2; :: thesis:

end;

assume A11: y in Y ; :: thesis:
assume A12: [x,y] in f ; :: thesis:
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:

end;

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