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

now :: thesis: (f +* g) . x = f . x

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

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

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

end;

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

hence (f +* g) . x = f . x by Th11; :: thesis: verum

end;

end;

end;

hence (f +* g) . x = f . x ; :: thesis: verum