let f, g be Function; for A being set st f,g equal_outside A holds
(dom f) \ A = (dom g) \ A
let A be set ; ( f,g equal_outside A implies (dom f) \ A = (dom g) \ A )
assume A1:
f | ((dom f) \ A) = g | ((dom g) \ A)
; FUNCT_7:def 2 (dom f) \ A = (dom g) \ A
thus (dom f) \ A =
(dom f) /\ ((dom f) \ A)
by XBOOLE_1:28
.=
dom (f | ((dom f) \ A))
by RELAT_1:61
.=
(dom g) /\ ((dom g) \ A)
by A1, RELAT_1:61
.=
(dom g) \ A
by XBOOLE_1:28
; verum