let n be Element of NAT ; :: thesis: for a, b, c, d, e being Real
for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= (n * e) * |.(d - c).|
let a, b, c, d, e be Real; :: thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= (n * e) * |.(d - c).|
let f be PartFunc of REAL,(REAL n); :: thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) implies |.(integral (f,c,d)).| <= (n * e) * |.(d - c).| )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) ) ; :: thesis: |.(integral (f,c,d)).| <= (n * e) * |.(d - c).|
A2: now :: thesis: for i being Element of NAT st i in Seg n holds
|.(integral (((proj (i,n)) * f),c,d)).| <= e * |.(d - c).|
let i be Element of NAT ; :: thesis: ( i in Seg n implies |.(integral (((proj (i,n)) * f),c,d)).| <= e * |.(d - c).| )
set P = proj (i,n);
assume A3: i in Seg n ; :: thesis: |.(integral (((proj (i,n)) * f),c,d)).| <= e * |.(d - c).|
dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng f c= dom (proj (i,n)) ;
then A4: ['a,b'] c= dom ((proj (i,n)) * f) by A1, RELAT_1:27;
set f1 = (proj (i,n)) * f;
A5: for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
|.(((proj (i,n)) * f) . x).| <= e
proof
let x be Real; :: thesis: ( x in ['(min (c,d)),(max (c,d))'] implies |.(((proj (i,n)) * f) . x).| <= e )
assume A6: x in ['(min (c,d)),(max (c,d))'] ; :: thesis: |.(((proj (i,n)) * f) . x).| <= e
['(min (c,d)),(max (c,d))'] c= ['a,b'] by A1, Lm2;
then A7: x in dom ((proj (i,n)) * f) by A4, A6;
then A8: x in dom f by FUNCT_1:11;
A9: |.(f /. x).| <= e by A1, A6;
A10: ((proj (i,n)) * f) . x = (proj (i,n)) . (f . x) by A7, FUNCT_1:12
.= (proj (i,n)) . (f /. x) by A8, PARTFUN1:def 6 ;
( 1 <= i & i <= n ) by A3, FINSEQ_1:1;
then |.((proj (i,n)) . (f /. x)).| <= |.(f /. x).| by PDIFF_8:5;
hence |.(((proj (i,n)) * f) . x).| <= e by A10, A9, XXREAL_0:2; :: thesis: verum
end;
A11: (proj (i,n)) * f is_integrable_on ['a,b'] by A1, A3;
A12: (proj (i,n)) * (f | ['a,b']) is bounded by A1, A3;
((proj (i,n)) * f) | ['a,b'] = (proj (i,n)) * (f | ['a,b']) by RELAT_1:83;
hence |.(integral (((proj (i,n)) * f),c,d)).| <= e * |.(d - c).| by A12, A1, A4, A5, A11, Lm4; :: thesis: verum
end;
now :: thesis: for i being Element of NAT st 1 <= i & i <= n holds
|.((integral (f,c,d)) . i).| <= e * |.(d - c).|
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies |.((integral (f,c,d)) . i).| <= e * |.(d - c).| )
set P = proj (i,n);
assume ( 1 <= i & i <= n ) ; :: thesis: |.((integral (f,c,d)) . i).| <= e * |.(d - c).|
then A13: i in Seg n ;
then |.(integral (((proj (i,n)) * f),c,d)).| <= e * |.(d - c).| by A2;
hence |.((integral (f,c,d)) . i).| <= e * |.(d - c).| by A13, INTEGR15:def 18; :: thesis: verum
end;
then |.(integral (f,c,d)).| <= n * (e * |.(d - c).|) by PDIFF_8:15;
hence |.(integral (f,c,d)).| <= (n * e) * |.(d - c).| ; :: thesis: verum