theorem Lm29d: :: FUZZY_7:49

for a1, c, a2, d being Real
for f being Function of REAL,REAL st c > 0 & d > 0 & a1 < a2 & f | [.(a1 - c),(a2 + c).] = (((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.]) +* ((AffineMap (0,d)) | [.a1,a2.])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) holds
integral (f,['(a1 - c),(a2 + c)']) = ((integral ((AffineMap ((d / c),(- ((d / c) * (a1 - c))))),['(a1 - c),a1'])) + (integral ((AffineMap (0,d)),['a1,a2']))) + (integral ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))),['a2,(a2 + c)']))