let n be Element of NAT ; 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; 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); ( 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 )
; ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )
A2:
now 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 ;
( 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
;
( (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;
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']
; 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
; verum