let f, g, h be Function; :: thesis: for A being set st f,g equal_outside A holds
f +* h,g +* h equal_outside A
let A be set ; :: thesis: ( f,g equal_outside A implies f +* h,g +* h equal_outside A )
A1: dom ((f +* h) | ((dom (f +* h)) \ A)) = (dom (f +* h)) \ A by RELAT_1:156
.= ((dom f) \/ (dom h)) \ A by FUNCT_4:def 1
.= ((dom f) \ A) \/ ((dom h) \ A) by XBOOLE_1:42 ;
assume f,g equal_outside A ; :: thesis: f +* h,g +* h equal_outside A
then A2: f | ((dom f) \ A) = g | ((dom g) \ A) ;
then A3: (dom f) \ A = dom (g | ((dom g) \ A)) by RELAT_1:156
.= (dom g) \ A by RELAT_1:156 ;
then A4: dom ((f +* h) | ((dom (f +* h)) \ A)) = ((dom g) \/ (dom h)) \ A by A1, XBOOLE_1:42
.= (dom (g +* h)) \ A by FUNCT_4:def 1
.= dom ((g +* h) | ((dom (g +* h)) \ A)) by RELAT_1:156 ;

now :: thesis: for x being object st x in dom ((f +* h) | ((dom (f +* h)) \ A)) holds
((f +* h) | ((dom (f +* h)) \ A)) . x = ((g +* h) | ((dom (g +* h)) \ A)) . x

let x be object ; :: thesis: ( x in dom ((f +* h) | ((dom (f +* h)) \ A)) implies ((f +* h) | ((dom (f +* h)) \ A)) . b₁ = ((g +* h) | ((dom (g +* h)) \ A)) . b₁ )
assume A5: x in dom ((f +* h) | ((dom (f +* h)) \ A)) ; :: thesis: ((f +* h) | ((dom (f +* h)) \ A)) . b₁ = ((g +* h) | ((dom (g +* h)) \ A)) . b₁
then A6: ( x in (dom f) \ A or x in (dom h) \ A ) by A1, XBOOLE_0:def 3;

per cases ( x in (dom h) \ A or not x in (dom h) \ A ) ;

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

thus ((f +* h) | ((dom (f +* h)) \ A)) . x = (f +* h) . x by A5, FUNCT_1:47
.= h . x by A7, FUNCT_4:13
.= (g +* h) . x by A7, FUNCT_4:13
.= ((g +* h) | ((dom (g +* h)) \ A)) . x by A4, A5, FUNCT_1:47 ; :: thesis: verum

end;

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

not x in A by A6, XBOOLE_0:def 5;
then A9: not x in dom h by A8, XBOOLE_0:def 5;
A10: x in (dom f) \ A by A1, A5, A8, XBOOLE_0:def 3;
thus ((f +* h) | ((dom (f +* h)) \ A)) . x = (f +* h) . x by A5, FUNCT_1:47
.= f . x by A9, FUNCT_4:11
.= (g | ((dom g) \ A)) . x by A2, A6, A8, FUNCT_1:49
.= g . x by A3, A10, FUNCT_1:49
.= (g +* h) . x by A9, FUNCT_4:11
.= ((g +* h) | ((dom (g +* h)) \ A)) . x by A4, A5, FUNCT_1:47 ; :: thesis: verum

end;

end;

end;

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