let g, f be Function; :: thesis: ( g c= f implies f | (dom g) = g )
assume A1: g c= f ; :: thesis: f | (dom g) = g
for x, y being set st [x,y] in f | (dom g) holds
[x,y] in g

proof

let x, y be set ; :: thesis: ( [x,y] in f | (dom g) implies [x,y] in g )
assume A2: [x,y] in f | (dom g) ; :: thesis: [x,y] in g
then x in dom g by RELAT_1:def 11;
then A3: [x,(g . x)] in g by FUNCT_1:def 2;
[x,y] in f by A2, RELAT_1:def 11;
hence [x,y] in g by A1, A3, FUNCT_1:def 1; :: thesis: verum

end;

then A4: f | (dom g) c= g by RELAT_1:def 3;
g | (dom g) c= f | (dom g) by A1, RELAT_1:76;
then g c= f | (dom g) by RELAT_1:68;
hence f | (dom g) = g by A4, XBOOLE_0:def 10; :: thesis: verum