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 )
assume A1: dom g misses D ; :: thesis: (f +* g) | D = f | D
A2: 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 A1, XBOOLE_0:def 7
.= (dom f) /\ D ;
A3: dom (f | D) = (dom f) /\ D by RELAT_1:90;

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 dom f & x in D ) by XBOOLE_0:def 4;
then A5: not x in dom g by A1, 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;

hence (f +* g) | D = f | D by A2, A3, FUNCT_1:9; :: thesis: verum