let f, g 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 object st [x,y] in f | (dom g) holds
[x,y] in g

proof

let x, y be object ; :: 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 ;
g | (dom g) c= f | (dom g) by A1, RELAT_1:76;
then g c= f | (dom g) ;
hence f | (dom g) = g by A4; :: thesis: verum