let f, g be Function; ( g c= f implies f | (dom g) = g )
assume A1:
g c= f
; 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 ;
( [x,y] in f | (dom g) implies [x,y] in g )
assume A2:
[x,y] in f | (dom g)
;
[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;
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; verum