A1: for x being set st x in dom f holds
(f +* g) . x = f . x

proof

let x be set ; :: thesis: ( x in dom f implies (f +* g) . x = f . x )
assume x in dom f ; :: thesis: (f +* g) . x = f . x
then x in (dom f) \ (dom g) ;
hence (f +* g) . x = f . x by Th11; :: thesis: verum

end;

(dom f) \/ (dom g) = dom f ;
then dom (f +* g) = dom f by Def1;
hence f +* g = f by A1, FUNCT_1:2; :: thesis: verum