theorem Th24: :: FUZZY_8:38

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 (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']))