theorem Th23: :: FUZZY_8:37

for a, b, c, d, r, s being Real
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 (((id REAL) (#) f),['a,d']) = ((integral (((id REAL) (#) (AffineMap ((r / (b - a)),(- ((a * r) / (b - a)))))),['a,b'])) + (integral (((id REAL) (#) (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b)))))),['b,c']))) + (integral (((id REAL) (#) (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c)))))),['c,d']))