theorem :: FUZZY_7:40

for a1, c, a2, d being Real
for f being Function of REAL,REAL st c > 0 & d > 0 & a1 < a2 & f = (d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | ['(a1 - c),(a2 + c)'] holds
f is_integrable_on ['(a1 - c),(a2 + c)']