let f, g be Function; :: thesis: (f +* g) | (dom g) = g
(dom f) \/ (dom g) = dom (f +* g) by Def1;
then A1: dom ((f +* g) | (dom g)) = dom g by RELAT_1:91, XBOOLE_1:7;
for x being set st x in dom g holds
((f +* g) | (dom g)) . x = g . x

proof

let x be set ; :: thesis: ( x in dom g implies ((f +* g) | (dom g)) . x = g . x )
( x in dom g implies (f +* g) . x = g . x ) by Th14;
hence ( x in dom g implies ((f +* g) | (dom g)) . x = g . x ) by A1, FUNCT_1:70; :: thesis: verum

end;

hence (f +* g) | (dom g) = g by A1, FUNCT_1:9; :: thesis: verum