let n be Element of NAT ; :: thesis: for a, b being Real
for f being PartFunc of REAL,(REAL n)
for E being Element of REAL n st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds
f . x = E ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )
let a, b be Real; :: thesis: for f being PartFunc of REAL,(REAL n)
for E being Element of REAL n st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds
f . x = E ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )
let f be PartFunc of REAL,(REAL n); :: thesis: for E being Element of REAL n st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds
f . x = E ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )
let E be Element of REAL n; :: thesis: ( a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds
f . x = E ) implies ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E ) )
assume A1: ( a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds
f . x = E ) ) ; :: thesis: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )

A2: now :: thesis: for i being Element of NAT st i in Seg n holds
( (proj (i,n)) * f is_integrable_on ['a,b'] & ((proj (i,n)) * f) | ['a,b'] is bounded & integral (((proj (i,n)) * f),a,b) = ((proj (i,n)) . E) * (b - a) )

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( (proj (i,n)) * f is_integrable_on ['a,b'] & ((proj (i,n)) * f) | ['a,b'] is bounded & integral (((proj (i,n)) * f),a,b) = ((proj (i,n)) . E) * (b - a) ) )
set P = proj (i,n);
assume i in Seg n ; :: thesis: ( (proj (i,n)) * f is_integrable_on ['a,b'] & ((proj (i,n)) * f) | ['a,b'] is bounded & integral (((proj (i,n)) * f),a,b) = ((proj (i,n)) . E) * (b - a) )
dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng f c= dom (proj (i,n)) ;
then A3: ['a,b'] c= dom ((proj (i,n)) * f) by A1, RELAT_1:27;
for x being Real st x in ['a,b'] holds
((proj (i,n)) * f) . x = (proj (i,n)) . E

proof

let x be Real; :: thesis: ( x in ['a,b'] implies ((proj (i,n)) * f) . x = (proj (i,n)) . E )
assume A4: x in ['a,b'] ; :: thesis: ((proj (i,n)) * f) . x = (proj (i,n)) . E
A5: f . x = f /. x by A4, A1, PARTFUN1:def 6;
hence ((proj (i,n)) * f) . x = (proj (i,n)) . (f /. x) by A4, A3, FUNCT_1:12
.= (proj (i,n)) . E by A4, A1, A5 ;
:: thesis: verum

end;

hence ( (proj (i,n)) * f is_integrable_on ['a,b'] & ((proj (i,n)) * f) | ['a,b'] is bounded & integral (((proj (i,n)) * f),a,b) = ((proj (i,n)) . E) * (b - a) ) by A3, A1, INTEGRA6:26; :: thesis: verum

end;

then A6: for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is_integrable_on ['a,b'] ;
A7: Seg n = dom (integral (f,a,b)) by INTEGR15:def 18;

A8: now :: thesis: for i being Element of NAT st i in Seg n holds
(proj (i,n)) * (f | ['a,b']) is bounded

let i be Element of NAT ; :: thesis: ( i in Seg n implies (proj (i,n)) * (f | ['a,b']) is bounded )
set P = proj (i,n);
assume i in Seg n ; :: thesis: (proj (i,n)) * (f | ['a,b']) is bounded
then ((proj (i,n)) * f) | ['a,b'] is bounded by A2;
hence (proj (i,n)) * (f | ['a,b']) is bounded by RELAT_1:83; :: thesis: verum

end;

A9: now :: thesis: for i being Nat st i in dom (integral (f,a,b)) holds
(integral (f,a,b)) . i = ((b - a) * E) . i

let i be Nat; :: thesis: ( i in dom (integral (f,a,b)) implies (integral (f,a,b)) . i = ((b - a) * E) . i )
assume A10: i in dom (integral (f,a,b)) ; :: thesis: (integral (f,a,b)) . i = ((b - a) * E) . i
hence (integral (f,a,b)) . i = integral (((proj (i,n)) * f),a,b) by A7, INTEGR15:def 18
.= ((proj (i,n)) . E) * (b - a) by A10, A2, A7
.= (b - a) * (E . i) by PDIFF_1:def 1
.= ((b - a) * E) . i by RVSUM_1:44 ;
:: thesis: verum

end;

len ((b - a) * E) = n by CARD_1:def 7;
then Seg n = dom ((b - a) * E) by FINSEQ_1:def 3;
hence ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E ) by A6, A8, A7, A9, FINSEQ_1:13; :: thesis: verum