let A be non empty closed_interval Subset of REAL; :: thesis: for a, b, c, d being Real st a < b & b < c & c < d holds
( TrapezoidalFS (a,b,c,d) is_integrable_on A & (TrapezoidalFS (a,b,c,d)) | A is bounded )
let a, b, c, d be Real; :: thesis: ( a < b & b < c & c < d implies ( TrapezoidalFS (a,b,c,d) is_integrable_on A & (TrapezoidalFS (a,b,c,d)) | A is bounded ) )
assume A1: ( a < b & b < c & c < d ) ; :: thesis: ( TrapezoidalFS (a,b,c,d) is_integrable_on A & (TrapezoidalFS (a,b,c,d)) | A is bounded )
reconsider f = TrapezoidalFS (a,b,c,d) as PartFunc of REAL,REAL ;
TrapezoidalFS (a,b,c,d) is Lipschitzian by FUZZY_5:87, A1;
then A6: f | A is continuous ;
dom f = REAL by FUNCT_2:def 1;
hence ( TrapezoidalFS (a,b,c,d) is_integrable_on A & (TrapezoidalFS (a,b,c,d)) | A is bounded ) by INTEGRA5:11, INTEGRA5:10, A6; :: thesis: verum