let a, b be Real; 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; ( 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 )
; 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 ;
( 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)
;
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;
verum
end;
hence
f tolerates g
by PARTFUN1:def 4; verum