let f, g, h be Function; :: thesis: for D being set st f | D = h | D holds
(h +* g) | D = (f +* g) | D
let D be set ; :: thesis: ( f | D = h | D implies (h +* g) | D = (f +* g) | D )
assume A1: f | D = h | D ; :: thesis: (h +* g) | D = (f +* g) | D
A2: dom ((f +* g) | D) = (dom (f +* g)) /\ D by RELAT_1:61
.= ((dom f) \/ (dom g)) /\ D by Def1 ;
A3: dom ((h +* g) | D) = (dom (h +* g)) /\ D by RELAT_1:61
.= ((dom h) \/ (dom g)) /\ D by Def1 ;
then A4: dom ((h +* g) | D) = ((dom h) /\ D) \/ ((dom g) /\ D) by XBOOLE_1:23
.= (dom (f | D)) \/ ((dom g) /\ D) by A1, RELAT_1:61
.= ((dom f) /\ D) \/ ((dom g) /\ D) by RELAT_1:61
.= ((dom f) \/ (dom g)) /\ D by XBOOLE_1:23 ;

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

let x be object ; :: thesis: ( x in dom ((f +* g) | D) implies ((h +* g) | D) . b₁ = ((f +* g) | D) . b₁ )
assume A5: x in dom ((f +* g) | D) ; :: thesis: ((h +* g) | D) . b₁ = ((f +* g) | D) . b₁
then A6: x in (dom f) \/ (dom g) by A2, XBOOLE_0:def 4;
A7: x in D by A2, A5, XBOOLE_0:def 4;
A8: ( x in (dom h) \/ (dom g) & ((h +* g) | D) . x = (h +* g) . x ) by A2, A3, A4, A5, FUNCT_1:47, XBOOLE_0:def 4;

per cases ( x in dom g or not x in dom g ) ;

suppose A9: x in dom g ; :: thesis: ((h +* g) | D) . b₁ = ((f +* g) | D) . b₁

((f +* g) | D) . x = (f +* g) . x by A5, FUNCT_1:47
.= g . x by A6, A9, Def1 ;
hence ((h +* g) | D) . x = ((f +* g) | D) . x by A8, A9, Def1; :: thesis: verum

end;

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

then A11: ((h +* g) | D) . x = h . x by A8, Def1
.= (h | D) . x by A7, FUNCT_1:49 ;
thus ((f +* g) | D) . x = (f +* g) . x by A5, FUNCT_1:47
.= f . x by A6, A10, Def1
.= ((h +* g) | D) . x by A1, A7, A11, FUNCT_1:49 ; :: thesis: verum

end;

end;

end;

hence (h +* g) | D = (f +* g) | D by A2, A4; :: thesis: verum