let f, g be Function; :: thesis: for x being object st not x in dom g holds
(f +* g) . x = f . x
let x be object ; :: thesis: ( not x in dom g implies (f +* g) . x = f . x )
assume A1: not x in dom g ; :: thesis: (f +* g) . x = f . x

per cases ( x in dom f or not x in dom f ) ;

suppose x in dom f ; :: thesis: (f +* g) . x = f . x

then x in (dom f) \/ (dom g) by XBOOLE_0:def 3;
hence (f +* g) . x = f . x by A1, Def1; :: thesis: verum

end;

suppose A2: not x in dom f ; :: thesis: (f +* g) . x = f . x

then not x in (dom f) \/ (dom g) by A1, XBOOLE_0:def 3;
then not x in dom (f +* g) by Def1;
hence (f +* g) . x = {} by FUNCT_1:def 2
.= f . x by A2, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;