let a, b, c, d, r, s be Real; :: thesis: for f being Function of REAL,REAL st a < b & b < c & c < d & f | [.a,d.] = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,d.]) holds
integral (f,['a,d']) = ((integral ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))),['a,b'])) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c']))) + (integral ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))),['c,d']))
let f be Function of REAL,REAL; :: thesis: ( a < b & b < c & c < d & f | [.a,d.] = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,d.]) implies integral (f,['a,d']) = ((integral ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))),['a,b'])) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c']))) + (integral ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))),['c,d'])) )
assume A1: ( a < b & b < c & c < d ) ; :: thesis: ( not f | [.a,d.] = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,d.]) or integral (f,['a,d']) = ((integral ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))),['a,b'])) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c']))) + (integral ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))),['c,d'])) )
assume A3: f | [.a,d.] = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,d.]) ; :: thesis: integral (f,['a,d']) = ((integral ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))),['a,b'])) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c']))) + (integral ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))),['c,d']))
set fab = AffineMap ((r / (b - a)),(- ((a * r) / (b - a))));
set fbc = AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))));
set fcd = AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))));
reconsider h = ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.[) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,+infty.[) as Function of REAL,REAL by FUZZY_6:18;
C2: (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . b = r by Th23a, A1
.= (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . b by Th23a, A1 ;
C1: dom (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) = (dom ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.])) \/ (dom ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) by FUNCT_4:def 1
.= [.a,b.] \/ (dom ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) by FUNCT_2:def 1
.= [.a,b.] \/ [.b,c.] by FUNCT_2:def 1
.= [.a,c.] by XXREAL_1:165, A1
.= dom (h | [.a,c.]) by FUNCT_2:def 1 ;
C3: for x being object st x in dom (h | [.a,c.]) holds
(h | [.a,c.]) . x = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) . x

proof

let x be object ; :: thesis: ( x in dom (h | [.a,c.]) implies (h | [.a,c.]) . x = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) . x )
assume D1: x in dom (h | [.a,c.]) ; :: thesis: (h | [.a,c.]) . x = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) . x
then x in [.a,c.] ;
then reconsider x = x as Element of REAL ;
D2: ( a <= x & x <= c ) by D1, XXREAL_1:1;

per cases ( x < b or x >= b ) ;

suppose S1: x < b ; :: thesis: (h | [.a,c.]) . x = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) . x

then G1: x in [.a,b.] by D2;
G2: not x in dom ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,+infty.[) by XXREAL_1:236, S1;
G6: not x in dom ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.]) by XXREAL_1:1, S1;
(h | [.a,c.]) . x = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.[) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,+infty.[)) . x by FUNCT_1:49, D1
.= ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.[) . x by FUNCT_4:11, G2
.= (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . x by FUNCT_1:49, XXREAL_1:233, S1
.= ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) . x by FUNCT_1:49, G1 ;
hence (h | [.a,c.]) . x = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) . x by FUNCT_4:11, G6; :: thesis: verum

end;

suppose S2: x >= b ; :: thesis: (h | [.a,c.]) . x = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) . x

then G3: x in [.b,c.] by D2;
x in [.b,+infty.[ by XXREAL_1:236, S2;
then G4: x in dom ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,+infty.[) by FUNCT_2:def 1;
G8: x in dom ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.]) by FUNCT_2:def 1, G3;
(h | [.a,c.]) . x = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.[) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,+infty.[)) . x by FUNCT_1:49, D1
.= ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,+infty.[) . x by FUNCT_4:13, G4
.= (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . x by FUNCT_1:49, XXREAL_1:236, S2
.= ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.]) . x by FUNCT_1:49, G3 ;
hence (h | [.a,c.]) . x = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) . x by FUNCT_4:13, G8; :: thesis: verum

end;

end;

end;

C4: integral (h,['a,c']) = (integral ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))),['a,b'])) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c'])) by F633, A1, C2, C3, FUNCT_1:2, C1;
B1: a <= c by A1, XXREAL_0:2;
c in [.b,+infty.[ by A1, XXREAL_1:236;
then c in dom ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,+infty.[) by FUNCT_2:def 1;
then B3: h . c = ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,+infty.[) . c by FUNCT_4:13
.= (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . c by FUNCT_1:49, A1, XXREAL_1:236
.= s by Th23a, A1
.= (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . c by Th23a, A1 ;
( AffineMap ((r / (b - a)),(- ((a * r) / (b - a)))) is Lipschitzian & AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b)))) is Lipschitzian ) by FUZZY_6:27;
then B2: h is Lipschitzian by FUZZY_6:26, C2;
f | [.a,d.] = (h | [.a,c.]) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,d.]) by C3, A3, FUNCT_1:2, C1;
hence integral (f,['a,d']) = ((integral ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))),['a,b'])) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c']))) + (integral ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))),['c,d'])) by C4, F633, B2, B3, A1, B1; :: thesis: verum