let n be Element of NAT ; :: thesis: for a, b, c, d, r being Real
for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded )
let a, b, c, d, r be Real; :: thesis: for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded )
let f be PartFunc of REAL,(REAL n); :: thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f implies ( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded ) )
assume that
A1: ( a <= c & c <= d & d <= b ) and
A2: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) and
A3: ['a,b'] c= dom f ; :: thesis: ( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded )

A4: now :: thesis: for i being Element of NAT st i in Seg n holds
( (proj (i,n)) * (r (#) f) is_integrable_on ['c,d'] & (proj (i,n)) * ((r (#) f) | ['c,d']) is bounded )

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( (proj (i,n)) * (r (#) f) is_integrable_on ['c,d'] & (proj (i,n)) * ((r (#) f) | ['c,d']) is bounded ) )
set P = proj (i,n);
assume A5: i in Seg n ; :: thesis: ( (proj (i,n)) * (r (#) f) is_integrable_on ['c,d'] & (proj (i,n)) * ((r (#) f) | ['c,d']) is bounded )
then A6: (proj (i,n)) * f is_integrable_on ['a,b'] by A2;
(proj (i,n)) * (f | ['a,b']) is bounded by A5, A2;
then A7: ((proj (i,n)) * f) | ['a,b'] is bounded by RELAT_1:83;
dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng f c= dom (proj (i,n)) ;
then A8: dom ((proj (i,n)) * f) = dom f by RELAT_1:27;
A9: ( r (#) ((proj (i,n)) * f) is_integrable_on ['c,d'] & (r (#) ((proj (i,n)) * f)) | ['c,d'] is bounded ) by A1, A3, Th6, A6, A7, A8;
(r (#) ((proj (i,n)) * f)) | ['c,d'] = ((proj (i,n)) * (r (#) f)) | ['c,d'] by INTEGR15:16
.= (proj (i,n)) * ((r (#) f) | ['c,d']) by RELAT_1:83 ;
hence ( (proj (i,n)) * (r (#) f) is_integrable_on ['c,d'] & (proj (i,n)) * ((r (#) f) | ['c,d']) is bounded ) by A9, INTEGR15:16; :: thesis: verum

end;

then for i being Element of NAT st i in Seg n holds
(proj (i,n)) * (r (#) f) is_integrable_on ['c,d'] ;
hence r (#) f is_integrable_on ['c,d'] ; :: thesis: (r (#) f) | ['c,d'] is bounded
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * ((r (#) f) | ['c,d']) is bounded by A4;
hence (r (#) f) | ['c,d'] is bounded ; :: thesis: verum