let f, g be Function; :: thesis: for D being set st dom g misses D holds
(f +* g) | D = f | D
let D be set ; :: thesis: ( dom g misses D implies (f +* g) | D = f | D )
A1: dom (f | D) = (dom f) /\ D by RELAT_1:90;
assume A2: dom g misses D ; :: thesis: (f +* g) | D = f | D

A3: now

let x be set ; :: thesis: ( x in (dom f) /\ D implies ((f +* g) | D) . x = (f | D) . x )
assume x in (dom f) /\ D ; :: thesis: ((f +* g) | D) . x = (f | D) . x
then A4: x in D by XBOOLE_0:def 4;
then A5: not x in dom g by A2, XBOOLE_0:3;
thus ((f +* g) | D) . x = (f +* g) . x by A4, FUNCT_1:72
.= f . x by A5, Th12
.= (f | D) . x by A4, FUNCT_1:72 ; :: thesis: verum

end;

dom ((f +* g) | D) = (dom (f +* g)) /\ D by RELAT_1:90
.= ((dom f) \/ (dom g)) /\ D by Def1
.= ((dom f) /\ D) \/ ((dom g) /\ D) by XBOOLE_1:23
.= ((dom f) /\ D) \/ {} by A2, XBOOLE_0:def 7
.= (dom f) /\ D ;
hence (f +* g) | D = f | D by A1, A3, FUNCT_1:9; :: thesis: verum