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