let x be object ; :: thesis: for f, g being Function st f . x = g . x holds
f | {x} tolerates g | {x}
let f, g be Function; :: thesis: ( f . x = g . x implies f | {x} tolerates g | {x} )
assume A1: f . x = g . x ; :: thesis: f | {x} tolerates g | {x}
let a be object ; :: according to PARTFUN1:def 4 :: thesis: ( a in (dom (f | {x})) /\ (dom (g | {x})) implies (f | {x}) . a = (g | {x}) . a )
set F = f | {x};
set G = g | {x};
assume a in (dom (f | {x})) /\ (dom (g | {x})) ; :: thesis: (f | {x}) . a = (g | {x}) . a
then a in dom (f | {x}) by XBOOLE_0:def 4;
then A2: a in {x} by RELAT_1:57;
then a = x by TARSKI:def 1;
hence (g | {x}) . a = f . a by A1, A2, FUNCT_1:49
.= (f | {x}) . a by A2, FUNCT_1:49 ;
:: thesis: verum