let a1, c, a2, d be Real; :: thesis: 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)']
let f be Function of REAL,REAL; :: thesis: ( c > 0 & d > 0 & a1 < a2 & f = (d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | ['(a1 - c),(a2 + c)'] implies f is_integrable_on ['(a1 - c),(a2 + c)'] )
assume that
A1: ( c > 0 & d > 0 & a1 < a2 ) and
A2: f = (d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | ['(a1 - c),(a2 + c)'] ; :: thesis: f is_integrable_on ['(a1 - c),(a2 + c)']
( a1 - c < a1 - 0 & a2 + 0 < a2 + c ) by A1, XREAL_1:15, XREAL_1:8;
then ((d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | ['(a1 - c),(a2 + c)']) | ['(a1 - c),(a2 + c)'] is integrable by A1, Lm22d, INTEGRA5:def 1;
hence f is_integrable_on ['(a1 - c),(a2 + c)'] by INTEGRA5:def 1, A2; :: thesis: verum