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

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

assume A1: g = Y | f ; :: thesis: ( ( for x being set 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 set st x in dom g holds
f . x = g . x ) )

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

let x be set ; :: 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 Def4;
then A3: [x,(g . x)] in f by A1, RELAT_1:def 12;
hence x in dom f by RELAT_1:def 4; :: thesis: f . x in Y
then f . x = g . x by A3, Def4;
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 Def4;
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 RELAT_1:def 4; :: thesis: verum

end;

let x be set ; :: 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 Def4;
then A5: [x,(g . x)] in f by A1, RELAT_1:def 12;
then x in dom f by RELAT_1:def 4;
hence f . x = g . x by A5, Def4; :: thesis: verum

end;

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

now

let x, y be set ; :: 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 RELAT_1:def 4;
then A10: y = g . x by A8, Def4
.= 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, Def4; :: 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 Th8;
x in dom f by A12, RELAT_1:def 4;
then A14: x in dom g by A6, A11, A13;
then y = g . x by A7, A13;
hence [x,y] in g by A14, Def4; :: thesis: verum

end;

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