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

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

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( (proj (i,n)) * (f + g) is_integrable_on ['c,d'] & (proj (i,n)) * ((f + g) | ['c,d']) is bounded ) )
set P = proj (i,n);
assume A5: i in Seg n ; :: thesis: ( (proj (i,n)) * (f + g) is_integrable_on ['c,d'] & (proj (i,n)) * ((f + g) | ['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;
A8: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng f c= dom (proj (i,n)) ;
then A9: dom ((proj (i,n)) * f) = dom f by RELAT_1:27;
A10: (proj (i,n)) * g is_integrable_on ['a,b'] by A5, A2;
(proj (i,n)) * (g | ['a,b']) is bounded by A5, A2;
then A11: ((proj (i,n)) * g) | ['a,b'] is bounded by RELAT_1:83;
rng g c= dom (proj (i,n)) by A8;
then dom ((proj (i,n)) * g) = dom g by RELAT_1:27;
then A12: ( ((proj (i,n)) * f) + ((proj (i,n)) * g) is_integrable_on ['c,d'] & (((proj (i,n)) * f) + ((proj (i,n)) * g)) | ['c,d'] is bounded ) by A1, A3, A6, A7, A9, A10, A11, INTEGRA6:19;
(((proj (i,n)) * f) + ((proj (i,n)) * g)) | ['c,d'] = ((proj (i,n)) * (f + g)) | ['c,d'] by INTEGR15:15
.= (proj (i,n)) * ((f + g) | ['c,d']) by RELAT_1:83 ;
hence ( (proj (i,n)) * (f + g) is_integrable_on ['c,d'] & (proj (i,n)) * ((f + g) | ['c,d']) is bounded ) by A12, INTEGR15:15; :: thesis: verum

end;

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