let Y be RealBanachSpace; :: thesis: for a, b, c, d, e being Real
for f being continuous PartFunc of REAL, the carrier of Y st c <= d & [.a,b.] c= dom f & c in [.a,b.] & d in [.a,b.] & ( for x being Real st x in [.c,d.] holds
||.(f /. x).|| <= e ) holds
||.(integral (f,c,d)).|| <= e * (d - c)
let a, b, c, d, e be Real; :: thesis: for f being continuous PartFunc of REAL, the carrier of Y st c <= d & [.a,b.] c= dom f & c in [.a,b.] & d in [.a,b.] & ( for x being Real st x in [.c,d.] holds
||.(f /. x).|| <= e ) holds
||.(integral (f,c,d)).|| <= e * (d - c)
let f be continuous PartFunc of REAL, the carrier of Y; :: thesis: ( c <= d & [.a,b.] c= dom f & c in [.a,b.] & d in [.a,b.] & ( for x being Real st x in [.c,d.] holds
||.(f /. x).|| <= e ) implies ||.(integral (f,c,d)).|| <= e * (d - c) )
assume that
A2: c <= d and
A3: ( [.a,b.] c= dom f & c in [.a,b.] & d in [.a,b.] & ( for x being Real st x in [.c,d.] holds
||.(f /. x).|| <= e ) ) ; :: thesis: ||.(integral (f,c,d)).|| <= e * (d - c)
A4: |.(d - c).| = d - c by ABSVALUE:def 1, A2, XREAL_1:48;
( min (c,d) = c & max (c,d) = d ) by A2, XXREAL_0:def 9, XXREAL_0:def 10;
hence ||.(integral (f,c,d)).|| <= e * (d - c) by A3, A4, Lm13a; :: thesis: verum