let A be set ; for f, g being A -defined Function holds f,g equal_outside A
let f, g be A -defined Function; f,g equal_outside A
dom g c= A
by RELAT_1:def 18;
then A:
(dom g) \ A = {}
by XBOOLE_1:37;
dom f c= A
by RELAT_1:def 18;
then
(dom f) \ A = {}
by XBOOLE_1:37;
hence f | ((dom f) \ A) =
{}
.=
g | ((dom g) \ A)
by A
;
FUNCT_7:def 2 verum