let f, g, h be Function; :: thesis: for A being set st f,g equal_outside A holds
h +* f,h +* g equal_outside A
let A be set ; :: thesis: ( f,g equal_outside A implies h +* f,h +* g equal_outside A )
assume f,g equal_outside A ; :: thesis: h +* f,h +* g equal_outside A
then A1: f | ((dom f) \ A) = g | ((dom g) \ A) by Def2;
then A2: (dom f) \ A = dom (g | ((dom g) \ A)) by RELAT_1:191
.= (dom g) \ A by RELAT_1:191 ;
A3: dom ((h +* f) | ((dom (h +* f)) \ A)) = (dom (h +* f)) \ A by RELAT_1:191
.= ((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:191 ;

now

let x be set ; :: thesis: ( x in dom ((h +* f) | ((dom (h +* f)) \ A)) implies ((h +* f) | ((dom (h +* f)) \ A)) . b₁ = ((h +* g) | ((dom (h +* g)) \ A)) . b₁ )
assume A5: x in dom ((h +* f) | ((dom (h +* f)) \ A)) ; :: thesis: ((h +* f) | ((dom (h +* f)) \ A)) . b₁ = ((h +* g) | ((dom (h +* g)) \ A)) . b₁
then 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 ; :: thesis: ((h +* f) | ((dom (h +* f)) \ A)) . b₁ = ((h +* g) | ((dom (h +* g)) \ A)) . b₁

thus ((h +* f) | ((dom (h +* f)) \ A)) . x = (h +* f) . x by A5, FUNCT_1:70
.= f . x by A7, FUNCT_4:14
.= (g | ((dom g) \ A)) . x by A1, A7, FUNCT_1:72
.= g . x by A2, A7, FUNCT_1:72
.= (h +* g) . x by A2, A7, FUNCT_4:14
.= ((h +* g) | ((dom (h +* g)) \ A)) . x by A4, A5, FUNCT_1:70 ; :: thesis: verum

end;

suppose A8: not x in (dom f) \ A ; :: thesis: ((h +* f) | ((dom (h +* f)) \ A)) . b₁ = ((h +* g) | ((dom (h +* g)) \ A)) . b₁

A9: 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:70
.= h . x by A10, FUNCT_4:12
.= (h +* g) . x by A11, FUNCT_4:12
.= ((h +* g) | ((dom (h +* g)) \ A)) . x by A4, A5, FUNCT_1:70 ; :: thesis: verum

end;

end;

end;

then (h +* f) | ((dom (h +* f)) \ A) = (h +* g) | ((dom (h +* g)) \ A) by A4, FUNCT_1:9;
hence h +* f,h +* g equal_outside A by Def2; :: thesis: verum