let a, b be Real; :: thesis: for f, g being PartFunc of REAL,REAL st not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 holds
f tolerates g
let f, g be PartFunc of REAL,REAL; :: thesis: ( not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 implies f tolerates g )
assume A1: ( not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 ) ; :: thesis: f tolerates g
REAL \ ].a,b.[ c= REAL ;
then REAL \ ].a,b.[ c= dom (AffineMap (0,0)) by FUNCT_2:def 1;
then A2: dom f = REAL \ ].a,b.[ by RELAT_1:62, A1
.= ].-infty,a.] \/ [.b,+infty.[ by XXREAL_1:398 ;
for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x

proof

let x be object ; :: thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x )
K2: b < +infty by XXREAL_0:9, XREAL_0:def 1;
K3: -infty < a by XXREAL_0:12, XREAL_0:def 1;
assume P1: x in (dom f) /\ (dom g) ; :: thesis: f . x = g . x
then x in ([.a,b.] /\ ].-infty,a.]) \/ ([.a,b.] /\ [.b,+infty.[) by XBOOLE_1:23, A1, A2;
then x in {a} \/ ([.a,b.] /\ [.b,+infty.[) by XXREAL_1:417, A1, XXREAL_1:29, K3;
then x in {a} \/ {b} by XXREAL_1:416, A1, XXREAL_1:29, K2;
then x in {a,b} by ENUMSET1:1;
then W1: g . x = 0 by A1, TARSKI:def 2;
reconsider xx = x as Real by P1;
x in dom f by P1, XBOOLE_0:def 4;
then f . x = (AffineMap (0,0)) . xx by A1, FUNCT_1:47;
hence f . x = g . x by Kici1, W1; :: thesis: verum

end;

hence f tolerates g by PARTFUN1:def 4; :: thesis: verum