let n be Element of NAT ; :: thesis: for a, b, c, d 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
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )
let a, b, c, d 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
( f is_integrable_on ['c,d'] & 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 ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded ) )
assume A1: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f ) ; :: thesis: ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )
A2: now :: thesis: for i being Element of NAT st i in Seg n holds
( (proj (i,n)) * f is_integrable_on ['c,d'] & (proj (i,n)) * (f | ['c,d']) is bounded )
let i be Element of NAT ; :: thesis: ( i in Seg n implies ( (proj (i,n)) * f is_integrable_on ['c,d'] & (proj (i,n)) * (f | ['c,d']) is bounded ) )
set P = proj (i,n);
assume A3: i in Seg n ; :: thesis: ( (proj (i,n)) * f is_integrable_on ['c,d'] & (proj (i,n)) * (f | ['c,d']) is bounded )
then A4: (proj (i,n)) * f is_integrable_on ['a,b'] by A1;
(proj (i,n)) * (f | ['a,b']) is bounded by A3, A1;
then A5: ((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 dom ((proj (i,n)) * f) = dom f by RELAT_1:27;
then ( (proj (i,n)) * f is_integrable_on ['c,d'] & ((proj (i,n)) * f) | ['c,d'] is bounded & ['c,d'] c= dom ((proj (i,n)) * f) ) by A4, A5, A1, INTEGRA6:18;
hence ( (proj (i,n)) * f is_integrable_on ['c,d'] & (proj (i,n)) * (f | ['c,d']) is bounded ) by RELAT_1:83; :: thesis: verum
end;
then for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is_integrable_on ['c,d'] ;
hence f is_integrable_on ['c,d'] ; :: thesis: f | ['c,d'] is bounded
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * (f | ['c,d']) is bounded by A2;
hence f | ['c,d'] is bounded ; :: thesis: verum