let x be set ; :: thesis: for g, f being Function st not x in dom g holds
(f +* g) . x = f . x
let g, f be Function; :: 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) & not x in dom g ) by A1, XBOOLE_0:def 3;
hence (f +* g) . x = f . x by 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 4
.= f . x by A2, FUNCT_1:def 4 ;
:: thesis: verum

end;

end;