let f, g be Function; for A being set st dom g c= A holds
f,f +* g equal_outside A
let A be set ; ( dom g c= A implies f,f +* g equal_outside A )
assume A1:
dom g c= A
; f,f +* g equal_outside A
A2: (dom (f +* g)) \ A =
((dom f) \/ (dom g)) \ A
by FUNCT_4:def 1
.=
((dom f) \ A) \/ ((dom g) \ A)
by XBOOLE_1:42
.=
((dom f) \ A) \/ {}
by A1, XBOOLE_1:37
.=
(dom f) \ A
;
(dom f) \ A misses A
by XBOOLE_1:79;
then
(dom f) \ A misses dom g
by A1, XBOOLE_1:63;
hence
f | ((dom f) \ A) = (f +* g) | ((dom (f +* g)) \ A)
by A2, FUNCT_4:72; FUNCT_7:def 2 verum