let f, g, h be Function; for A being set st f,g equal_outside A holds
h +* f,h +* g equal_outside A
let A be set ; ( f,g equal_outside A implies h +* f,h +* g equal_outside A )
assume
f,g equal_outside A
; h +* f,h +* g equal_outside A
then A1:
f | ((dom f) \ A) = g | ((dom g) \ A)
;
then A2: (dom f) \ A =
dom (g | ((dom g) \ A))
by RELAT_1:156
.=
(dom g) \ A
by RELAT_1:156
;
A3: dom ((h +* f) | ((dom (h +* f)) \ A)) =
(dom (h +* f)) \ A
by RELAT_1:156
.=
((dom h) \/ (dom f)) \ A
by FUNCT_4:def 1
.=
((dom h) \ A) \/ ((dom f) \ A)
by XBOOLE_1:42
;
then A4: dom ((h +* f) | ((dom (h +* f)) \ A)) =
((dom h) \/ (dom g)) \ A
by A2, XBOOLE_1:42
.=
(dom (h +* g)) \ A
by FUNCT_4:def 1
.=
dom ((h +* g) | ((dom (h +* g)) \ A))
by RELAT_1:156
;
now for x being object st x in dom ((h +* f) | ((dom (h +* f)) \ A)) holds
((h +* f) | ((dom (h +* f)) \ A)) . x = ((h +* g) | ((dom (h +* g)) \ A)) . xlet x be
object ;
( x in dom ((h +* f) | ((dom (h +* f)) \ A)) implies ((h +* f) | ((dom (h +* f)) \ A)) . b1 = ((h +* g) | ((dom (h +* g)) \ A)) . b1 )assume A5:
x in dom ((h +* f) | ((dom (h +* f)) \ A))
;
((h +* f) | ((dom (h +* f)) \ A)) . b1 = ((h +* g) | ((dom (h +* g)) \ A)) . b1then A6:
(
x in (dom h) \ A or
x in (dom f) \ A )
by A3, XBOOLE_0:def 3;
per cases
( x in (dom f) \ A or not x in (dom f) \ A )
;
suppose A7:
x in (dom f) \ A
;
((h +* f) | ((dom (h +* f)) \ A)) . b1 = ((h +* g) | ((dom (h +* g)) \ A)) . b1thus ((h +* f) | ((dom (h +* f)) \ A)) . x =
(h +* f) . x
by A5, FUNCT_1:47
.=
f . x
by A7, FUNCT_4:13
.=
(g | ((dom g) \ A)) . x
by A1, A7, FUNCT_1:49
.=
g . x
by A2, A7, FUNCT_1:49
.=
(h +* g) . x
by A2, A7, FUNCT_4:13
.=
((h +* g) | ((dom (h +* g)) \ A)) . x
by A4, A5, FUNCT_1:47
;
verum end; suppose A8:
not
x in (dom f) \ A
;
((h +* f) | ((dom (h +* f)) \ A)) . b1 = ((h +* g) | ((dom (h +* g)) \ A)) . b1A9:
not
x in A
by A6, XBOOLE_0:def 5;
then A10:
not
x in dom f
by A8, XBOOLE_0:def 5;
A11:
not
x in dom g
by A2, A8, A9, XBOOLE_0:def 5;
thus ((h +* f) | ((dom (h +* f)) \ A)) . x =
(h +* f) . x
by A5, FUNCT_1:47
.=
h . x
by A10, FUNCT_4:11
.=
(h +* g) . x
by A11, FUNCT_4:11
.=
((h +* g) | ((dom (h +* g)) \ A)) . x
by A4, A5, FUNCT_1:47
;
verum end; end; end;
then
(h +* f) | ((dom (h +* f)) \ A) = (h +* g) | ((dom (h +* g)) \ A)
by A4;
hence
h +* f,h +* g equal_outside A
; verum