let A be non empty closed_interval Subset of REAL; :: thesis: for a, b, c, d, r being Real st a < b & b < c & c < d holds
r (#) (TrapezoidalFS (a,b,c,d)) is_integrable_on A
let a, b, c, d, r be Real; :: thesis: ( a < b & b < c & c < d implies r (#) (TrapezoidalFS (a,b,c,d)) is_integrable_on A )
assume A1: ( a < b & b < c & c < d ) ; :: thesis: r (#) (TrapezoidalFS (a,b,c,d)) is_integrable_on A
reconsider f = TrapezoidalFS (a,b,c,d) as PartFunc of REAL,REAL ;
A2: ( f is_integrable_on A & f | A is bounded ) by Lm22c, A1;
REAL = dom f by FUNCT_2:def 1;
hence r (#) (TrapezoidalFS (a,b,c,d)) is_integrable_on A by A2, INTEGRA6:9; :: thesis: verum