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:62, XBOOLE_1:7;
for x being object st x in dom g holds
((f +* g) | (dom g)) . x = g . x

proof

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

end;

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