:: INTEGR19 semantic presentation begin Lm1: for n being Element of NAT for f, g being PartFunc of REAL,(REAL n) holds f - g = f + (- g) by NDIFF_4:1; theorem Th1: :: INTEGR19:1 for a, c, b being real number st a <= c & c <= b holds ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) proof let a, c, b be real number ; ::_thesis: ( a <= c & c <= b implies ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) ) assume that A1: a <= c and A2: c <= b ; ::_thesis: ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) A3: c in [.a,b.] by A1, A2, XXREAL_1:1; hence c in ['a,b'] by A1, A2, INTEGRA5:def_3, XXREAL_0:2; ::_thesis: ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) A4: ['c,b'] = [.c,b.] by A2, INTEGRA5:def_3; a <= b by A1, A2, XXREAL_0:2; then A5: ( a in [.a,b.] & b in [.a,b.] ) by XXREAL_1:1; ( ['a,b'] = [.a,b.] & ['a,c'] = [.a,c.] ) by A1, A2, INTEGRA5:def_3, XXREAL_0:2; hence ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) by A4, A3, A5, XXREAL_2:def_12; ::_thesis: verum end; theorem Th2: :: INTEGR19:2 for X being set for a, c, d, b being real number st a <= c & c <= d & d <= b & ['a,b'] c= X holds ['c,d'] c= X proof let X be set ; ::_thesis: for a, c, d, b being real number st a <= c & c <= d & d <= b & ['a,b'] c= X holds ['c,d'] c= X let a, c, d, b be real number ; ::_thesis: ( a <= c & c <= d & d <= b & ['a,b'] c= X implies ['c,d'] c= X ) assume that A1: ( a <= c & c <= d & d <= b ) and A2: ['a,b'] c= X ; ::_thesis: ['c,d'] c= X A3: ['c,d'] c= ['c,b'] by Th1, A1; c <= b by A1, XXREAL_0:2; then ['c,b'] c= ['a,b'] by Th1, A1; then ['c,d'] c= ['a,b'] by A3, XBOOLE_1:1; hence ['c,d'] c= X by A2, XBOOLE_1:1; ::_thesis: verum end; Lm2: for a, b, c, d being real number st a <= b & c in ['a,b'] & d in ['a,b'] holds ['(min (c,d)),(max (c,d))'] c= ['a,b'] proof let a, b, c, d be real number ; ::_thesis: ( a <= b & c in ['a,b'] & d in ['a,b'] implies ['(min (c,d)),(max (c,d))'] c= ['a,b'] ) assume A1: ( a <= b & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ['(min (c,d)),(max (c,d))'] c= ['a,b'] ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A2: ( a <= c & d <= b & a <= d & c <= b ) by A1, XXREAL_1:1; percases ( c <= d or not c <= d ) ; supposeA3: c <= d ; ::_thesis: ['(min (c,d)),(max (c,d))'] c= ['a,b'] then A4: ( c = min (c,d) & d = max (c,d) ) by XXREAL_0:def_9, XXREAL_0:def_10; A5: ['c,b'] c= ['a,b'] by A2, Th1; ['c,d'] c= ['c,b'] by A2, A3, Th1; hence ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A4, A5, XBOOLE_1:1; ::_thesis: verum end; supposeA6: not c <= d ; ::_thesis: ['(min (c,d)),(max (c,d))'] c= ['a,b'] then A7: ( d = min (c,d) & c = max (c,d) ) by XXREAL_0:def_9, XXREAL_0:def_10; A8: ['d,b'] c= ['a,b'] by A2, Th1; ['d,c'] c= ['d,b'] by A2, A6, Th1; hence ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A7, A8, XBOOLE_1:1; ::_thesis: verum end; end; end; theorem Th3: :: INTEGR19:3 for X being set for a, b, c, d being real number st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= X holds ['(min (c,d)),(max (c,d))'] c= X proof let X be set ; ::_thesis: for a, b, c, d being real number st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= X holds ['(min (c,d)),(max (c,d))'] c= X let a, b, c, d be real number ; ::_thesis: ( a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= X implies ['(min (c,d)),(max (c,d))'] c= X ) assume ( a <= b & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( not ['a,b'] c= X or ['(min (c,d)),(max (c,d))'] c= X ) then ['(min (c,d)),(max (c,d))'] c= ['a,b'] by Lm2; hence ( not ['a,b'] c= X or ['(min (c,d)),(max (c,d))'] c= X ) by XBOOLE_1:1; ::_thesis: verum end; theorem Th4: :: INTEGR19:4 for n being Element of NAT for a, c, d, b being real number for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds ['c,d'] c= dom (f + g) proof let n be Element of NAT ; ::_thesis: for a, c, d, b being real number for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds ['c,d'] c= dom (f + g) let a, c, d, b be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds ['c,d'] c= dom (f + g) let f, g be PartFunc of REAL,(REAL n); ::_thesis: ( a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g implies ['c,d'] c= dom (f + g) ) assume that A1: ( a <= c & c <= d & d <= b ) and A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) ; ::_thesis: ['c,d'] c= dom (f + g) dom (f + g) = (dom f) /\ (dom g) by VALUED_2:def_45; then ['a,b'] /\ ['a,b'] c= dom (f + g) by A2, XBOOLE_1:27; hence ['c,d'] c= dom (f + g) by A1, Th2; ::_thesis: verum end; theorem Th5: :: INTEGR19:5 for n being Element of NAT for a, c, d, b being real number for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds ['c,d'] c= dom (f - g) proof let n be Element of NAT ; ::_thesis: for a, c, d, b being real number for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds ['c,d'] c= dom (f - g) let a, c, d, b be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds ['c,d'] c= dom (f - g) let f, g be PartFunc of REAL,(REAL n); ::_thesis: ( a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g implies ['c,d'] c= dom (f - g) ) assume that A1: ( a <= c & c <= d & d <= b ) and A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) ; ::_thesis: ['c,d'] c= dom (f - g) dom (f - g) = (dom f) /\ (dom g) by VALUED_2:def_46; then ['a,b'] /\ ['a,b'] c= dom (f - g) by A2, XBOOLE_1:27; hence ['c,d'] c= dom (f - g) by A1, Th2; ::_thesis: verum end; Lm3: for X, Y, Z being non empty set for f being PartFunc of X,Y st Z c= dom f holds f | Z is Function of Z,Y proof let X, Y, Z be non empty set ; ::_thesis: for f being PartFunc of X,Y st Z c= dom f holds f | Z is Function of Z,Y let f be PartFunc of X,Y; ::_thesis: ( Z c= dom f implies f | Z is Function of Z,Y ) rng f c= Y ; then f is Function of (dom f),Y by FUNCT_2:2; hence ( Z c= dom f implies f | Z is Function of Z,Y ) by FUNCT_2:32; ::_thesis: verum end; theorem Th6: :: INTEGR19:6 for a, c, d, b, r being real number for f being PartFunc of REAL,REAL 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 ) proof let a, c, d, b, r be real number ; ::_thesis: for f being PartFunc of REAL,REAL 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; ::_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 and A2: ( c <= d & d <= b ) and A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) and A4: ['a,b'] c= dom f ; ::_thesis: ( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded ) A5: r is Real by XREAL_0:def_1; A6: f | ['c,d'] is bounded by A1, A2, A3, A4, INTEGRA6:18; A7: ['c,d'] c= dom f by A2, A1, Th2, A4; f is_integrable_on ['c,d'] by A1, A2, A3, A4, INTEGRA6:18; hence r (#) f is_integrable_on ['c,d'] by A6, A7, A5, INTEGRA6:9; ::_thesis: (r (#) f) | ['c,d'] is bounded thus (r (#) f) | ['c,d'] is bounded by A6, RFUNCT_1:80; ::_thesis: verum end; theorem :: INTEGR19:7 for a, c, d, b being real number for f, g being PartFunc of REAL,REAL 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 ) proof let a, c, d, b be real number ; ::_thesis: for f, g being PartFunc of REAL,REAL 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; ::_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 A1: ( 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 ) ; ::_thesis: ( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded ) A2: ((- 1) (#) g) | ['a,b'] is bounded by A1, RFUNCT_1:80; A3: ['a,b'] c= dom ((- 1) (#) g) by A1, VALUED_1:def_5; - 1 is Real by XREAL_0:def_1; then (- 1) (#) g is_integrable_on ['a,b'] by A1, INTEGRA6:9; hence ( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded ) by A1, A2, A3, INTEGRA6:19; ::_thesis: verum end; Lm4: for a, b, c, d, e being real number for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds abs (f . x) <= e ) holds abs (integral (f,c,d)) <= e * (abs (d - c)) proof let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds abs (f . x) <= e ) holds abs (integral (f,c,d)) <= e * (abs (d - c)) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds abs (f . x) <= e ) implies abs (integral (f,c,d)) <= e * (abs (d - c)) ) set A = ['(min (c,d)),(max (c,d))']; assume that A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) and A2: for x being real number st x in ['(min (c,d)),(max (c,d))'] holds abs (f . x) <= e ; ::_thesis: abs (integral (f,c,d)) <= e * (abs (d - c)) rng (abs f) c= REAL ; then A3: abs f is Function of (dom (abs f)),REAL by FUNCT_2:2; ['(min (c,d)),(max (c,d))'] c= dom (abs f) by A1, INTEGRA6:21; then reconsider g = (abs f) | ['(min (c,d)),(max (c,d))'] as Function of ['(min (c,d)),(max (c,d))'],REAL by A3, FUNCT_2:32; A4: vol ['(min (c,d)),(max (c,d))'] = abs (d - c) by INTEGRA6:6; abs f is_integrable_on ['(min (c,d)),(max (c,d))'] by A1, INTEGRA6:21; then A5: g is integrable by INTEGRA5:def_1; e is Real by XREAL_0:def_1; then consider h being Function of ['(min (c,d)),(max (c,d))'],REAL such that A6: rng h = {e} and A7: h | ['(min (c,d)),(max (c,d))'] is bounded by INTEGRA4:5; A8: now__::_thesis:_for_x_being_Real_st_x_in_['(min_(c,d)),(max_(c,d))']_holds_ g_._x_<=_h_._x let x be Real; ::_thesis: ( x in ['(min (c,d)),(max (c,d))'] implies g . x <= h . x ) assume A9: x in ['(min (c,d)),(max (c,d))'] ; ::_thesis: g . x <= h . x then g . x = (abs f) . x by FUNCT_1:49; then A10: g . x = abs (f . x) by VALUED_1:18; h . x in {e} by A6, A9, FUNCT_2:4; then h . x = e by TARSKI:def_1; hence g . x <= h . x by A2, A9, A10; ::_thesis: verum end; A11: abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) by A1, INTEGRA6:21; ( min (c,d) <= c & c <= max (c,d) ) by XXREAL_0:17, XXREAL_0:25; then min (c,d) <= max (c,d) by XXREAL_0:2; then A12: integral ((abs f),(min (c,d)),(max (c,d))) = integral ((abs f),['(min (c,d)),(max (c,d))']) by INTEGRA5:def_4; (abs f) | ['(min (c,d)),(max (c,d))'] is bounded by A1, INTEGRA6:21; then A13: g | ['(min (c,d)),(max (c,d))'] is bounded ; e is Real by XREAL_0:def_1; then ( h is integrable & integral h = e * (vol ['(min (c,d)),(max (c,d))']) ) by A6, INTEGRA4:4; then integral ((abs f),(min (c,d)),(max (c,d))) <= e * (abs (d - c)) by A12, A7, A8, A5, A13, A4, INTEGRA2:34; hence abs (integral (f,c,d)) <= e * (abs (d - c)) by A11, XXREAL_0:2; ::_thesis: verum end; Lm5: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st A c= dom f holds f | A is Function of A,REAL by Lm3; theorem :: INTEGR19:8 for n being Element of NAT for a, b, c being real number for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] holds ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) proof let n be Element of NAT ; ::_thesis: for a, b, c being real number for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] holds ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) let a, b, c be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] holds ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] implies ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) ) assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] ) ; ::_thesis: ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ (_(proj_(i,n))_*_f_is_integrable_on_['a,c']_&_(proj_(i,n))_*_f_is_integrable_on_['c,b']_&_integral_(((proj_(i,n))_*_f),a,b)_=_(integral_(((proj_(i,n))_*_f),a,c))_+_(integral_(((proj_(i,n))_*_f),c,b))_) let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( (proj (i,n)) * f is_integrable_on ['a,c'] & (proj (i,n)) * f is_integrable_on ['c,b'] & integral (((proj (i,n)) * f),a,b) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) ) ) set P = proj (i,n); assume A3: i in Seg n ; ::_thesis: ( (proj (i,n)) * f is_integrable_on ['a,c'] & (proj (i,n)) * f is_integrable_on ['c,b'] & integral (((proj (i,n)) * f),a,b) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) ) then A4: (proj (i,n)) * f is_integrable_on ['a,b'] by A1, INTEGR15:def_16; (proj (i,n)) * (f | ['a,b']) is bounded by A3, A1, INTEGR15:def_15; 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; hence ( (proj (i,n)) * f is_integrable_on ['a,c'] & (proj (i,n)) * f is_integrable_on ['c,b'] & integral (((proj (i,n)) * f),a,b) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) ) by A4, A5, A1, INTEGRA6:17; ::_thesis: verum end; then for i being Element of NAT st i in Seg n holds (proj (i,n)) * f is_integrable_on ['a,c'] ; hence f is_integrable_on ['a,c'] by INTEGR15:def_16; ::_thesis: ( f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) for i being Element of NAT st i in Seg n holds (proj (i,n)) * f is_integrable_on ['c,b'] by A2; hence f is_integrable_on ['c,b'] by INTEGR15:def_16; ::_thesis: integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) A6: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(integral_(f,a,b))_holds_ (integral_(f,a,b))_._i_=_((integral_(f,a,c))_+_(integral_(f,c,b)))_._i let i be Nat; ::_thesis: ( i in dom (integral (f,a,b)) implies (integral (f,a,b)) . i = ((integral (f,a,c)) + (integral (f,c,b))) . i ) assume i in dom (integral (f,a,b)) ; ::_thesis: (integral (f,a,b)) . i = ((integral (f,a,c)) + (integral (f,c,b))) . i then A7: i in Seg n by INTEGR15:def_18; set P = proj (i,n); thus (integral (f,a,b)) . i = integral (((proj (i,n)) * f),a,b) by A7, INTEGR15:def_18 .= (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) by A7, A2 .= ((integral (f,a,c)) . i) + (integral (((proj (i,n)) * f),c,b)) by A7, INTEGR15:def_18 .= ((integral (f,a,c)) . i) + ((integral (f,c,b)) . i) by A7, INTEGR15:def_18 .= ((integral (f,a,c)) + (integral (f,c,b))) . i by RVSUM_1:11 ; ::_thesis: verum end; A8: Seg n = dom (integral (f,a,b)) by INTEGR15:def_18; len ((integral (f,a,c)) + (integral (f,c,b))) = n by CARD_1:def_7; then Seg n = dom ((integral (f,a,c)) + (integral (f,c,b))) by FINSEQ_1:def_3; hence integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by A8, A6, FINSEQ_1:13; ::_thesis: verum end; theorem Th9: :: INTEGR19:9 for n being Element of NAT for a, c, d, b being real number 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 ) proof let n be Element of NAT ; ::_thesis: for a, c, d, b being real number 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, c, d, b be real number ; ::_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, INTEGR15:def_16; (proj (i,n)) * (f | ['a,b']) is bounded by A3, A1, INTEGR15:def_15; 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'] by INTEGR15:def_16; ::_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 by INTEGR15:def_15; ::_thesis: verum end; theorem Th10: :: INTEGR19:10 for n being Element of NAT for a, c, d, b being real number 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 ) proof let n be Element of NAT ; ::_thesis: for a, c, d, b being real number 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, c, d, b be real number ; ::_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, INTEGR15:def_16; (proj (i,n)) * (f | ['a,b']) is bounded by A5, A2, INTEGR15:def_15; 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, INTEGR15:def_16; (proj (i,n)) * (g | ['a,b']) is bounded by A5, A2, INTEGR15:def_15; 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'] by INTEGR15:def_16; ::_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 by INTEGR15:def_15; ::_thesis: verum end; theorem Th11: :: INTEGR19:11 for n being Element of NAT for a, c, d, b, r being real number 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 ) proof let n be Element of NAT ; ::_thesis: for a, c, d, b, r being real number 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, c, d, b, r be real number ; ::_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, INTEGR15:def_16; (proj (i,n)) * (f | ['a,b']) is bounded by A5, A2, INTEGR15:def_15; 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; A10: r is Real by XREAL_0:def_1; then (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 A10, 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'] by INTEGR15:def_16; ::_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 by INTEGR15:def_15; ::_thesis: verum end; theorem Th12: :: INTEGR19:12 for n being Element of NAT for a, c, d, b being real number 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 ) proof let n be Element of NAT ; ::_thesis: for a, c, d, b being real number 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, c, d, b be real number ; ::_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 ) ) - f = (- 1) (#) f by NFCONT_4:7; hence ( 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 ) ) by Th11; ::_thesis: verum end; theorem Th13: :: INTEGR19:13 for n being Element of NAT for a, c, d, b being real number 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 ) proof let n be Element of NAT ; ::_thesis: for a, c, d, b being real number 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, c, d, b be real number ; ::_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: dom g = dom (- g) by NFCONT_4:def_3; A5: f - g = f + (- g) by Lm1; a <= d by A1, XXREAL_0:2; then a <= b by A1, XXREAL_0:2; then ( - g is_integrable_on ['a,b'] & (- g) | ['a,b'] is bounded ) by A2, A3, Th12; hence ( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded ) by A5, A1, A2, A3, A4, Th10; ::_thesis: verum end; theorem Th14: :: INTEGR19:14 for A being non empty closed_interval Subset of REAL for n being non empty Element of NAT for f being Function of A,(REAL n) holds ( f is bounded iff |.f.| is bounded ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for n being non empty Element of NAT for f being Function of A,(REAL n) holds ( f is bounded iff |.f.| is bounded ) let n be non empty Element of NAT ; ::_thesis: for f being Function of A,(REAL n) holds ( f is bounded iff |.f.| is bounded ) let f be Function of A,(REAL n); ::_thesis: ( f is bounded iff |.f.| is bounded ) hereby ::_thesis: ( |.f.| is bounded implies f is bounded ) assume A1: f is bounded ; ::_thesis: |.f.| is bounded defpred S1[ Nat, set ] means ex K being Element of REAL st ( 0 <= K & K = $2 & ( for y being set st y in dom ((proj ($1,n)) * f) holds abs (((proj ($1,n)) * f) . y) < K ) ); A2: for i being Nat st i in Seg n holds ex r being Element of REAL st S1[i,r] proof let i be Nat; ::_thesis: ( i in Seg n implies ex r being Element of REAL st S1[i,r] ) assume A3: i in Seg n ; ::_thesis: ex r being Element of REAL st S1[i,r] set P = proj (i,n); (proj (i,n)) * f is bounded by A1, A3, INTEGR15:def_12; then consider L being real number such that A4: for y being set st y in dom ((proj (i,n)) * f) holds abs (((proj (i,n)) * f) . y) < L by COMSEQ_2:def_3; now__::_thesis:_for_y_being_set_st_y_in_dom_((proj_(i,n))_*_f)_holds_ abs_(((proj_(i,n))_*_f)_._y)_<_abs_L let y be set ; ::_thesis: ( y in dom ((proj (i,n)) * f) implies abs (((proj (i,n)) * f) . y) < abs L ) assume A5: y in dom ((proj (i,n)) * f) ; ::_thesis: abs (((proj (i,n)) * f) . y) < abs L L <= abs L by ABSVALUE:4; hence abs (((proj (i,n)) * f) . y) < abs L by A4, A5, XXREAL_0:2; ::_thesis: verum end; hence ex r being Element of REAL st S1[i,r] by COMPLEX1:46; ::_thesis: verum end; consider w being FinSequence of REAL such that A6: ( dom w = Seg n & ( for i being Nat st i in Seg n holds S1[i,w . i] ) ) from FINSEQ_1:sch_5(A2); A7: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ (_0_<=_w_._i_&_(_for_y_being_set_st_y_in_dom_((proj_(i,n))_*_f)_holds_ abs_(((proj_(i,n))_*_f)_._y)_<_w_._i_)_) let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( 0 <= w . i & ( for y being set st y in dom ((proj (i,n)) * f) holds abs (((proj (i,n)) * f) . y) < w . i ) ) ) set P = proj (i,n); assume i in Seg n ; ::_thesis: ( 0 <= w . i & ( for y being set st y in dom ((proj (i,n)) * f) holds abs (((proj (i,n)) * f) . y) < w . i ) ) then S1[i,w . i] by A6; hence ( 0 <= w . i & ( for y being set st y in dom ((proj (i,n)) * f) holds abs (((proj (i,n)) * f) . y) < w . i ) ) ; ::_thesis: verum end; len w = n by A6, FINSEQ_1:def_3; then reconsider w = w as Element of REAL n by FINSEQ_2:92; A8: for i being Element of NAT st i in Seg n holds 0 <= w . i by A7; set KK = Sum w; for y being set st y in dom |.f.| holds abs (|.f.| . y) < (n * (Sum w)) + 1 proof let y be set ; ::_thesis: ( y in dom |.f.| implies abs (|.f.| . y) < (n * (Sum w)) + 1 ) assume A9: y in dom |.f.| ; ::_thesis: abs (|.f.| . y) < (n * (Sum w)) + 1 then A10: |.f.| . y = |.f.| /. y by PARTFUN1:def_6 .= |.(f /. y).| by A9, NFCONT_4:def_2 ; then A11: abs (|.f.| . y) = |.f.| . y by ABSVALUE:def_1; now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_n_holds_ |.((proj_(i,n))_._(f_/._y)).|_<=_Sum_w let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies |.((proj (i,n)) . (f /. y)).| <= Sum w ) set P = proj (i,n); assume A12: ( 1 <= i & i <= n ) ; ::_thesis: |.((proj (i,n)) . (f /. y)).| <= Sum w A13: y in dom f by A9, NFCONT_4:def_2; then f . y in rng f by FUNCT_1:3; then f . y in REAL n ; then f . y in dom (proj (i,n)) by FUNCT_2:def_1; then A14: y in dom ((proj (i,n)) * f) by A13, FUNCT_1:11; A15: i in Seg n by A12; then abs (((proj (i,n)) * f) . y) < w . i by A7, A14; then abs ((proj (i,n)) . (f . y)) < w . i by A14, FUNCT_1:12; then A16: |.((proj (i,n)) . (f /. y)).| < w . i by A13, PARTFUN1:def_6; w . i <= Sum w by A8, A15, REAL_NS1:7; hence |.((proj (i,n)) . (f /. y)).| <= Sum w by A16, XXREAL_0:2; ::_thesis: verum end; then |.(f /. y).| <= n * (Sum w) by PDIFF_8:17; then 0 + (abs (|.f.| . y)) < (n * (Sum w)) + 1 by A10, A11, XREAL_1:8; hence abs (|.f.| . y) < (n * (Sum w)) + 1 ; ::_thesis: verum end; hence |.f.| is bounded by COMSEQ_2:def_3; ::_thesis: verum end; assume |.f.| is bounded ; ::_thesis: f is bounded then consider K being real number such that A17: for y being set st y in dom |.f.| holds abs (|.f.| . y) < K by COMSEQ_2:def_3; let i be Element of NAT ; :: according to INTEGR15:def_12 ::_thesis: ( not i in Seg n or (proj (i,n)) * f is bounded ) set P = proj (i,n); assume A18: i in Seg n ; ::_thesis: (proj (i,n)) * f is bounded for y being set st y in dom ((proj (i,n)) * f) holds abs (((proj (i,n)) * f) . y) < K proof let y be set ; ::_thesis: ( y in dom ((proj (i,n)) * f) implies abs (((proj (i,n)) * f) . y) < K ) assume A19: y in dom ((proj (i,n)) * f) ; ::_thesis: abs (((proj (i,n)) * f) . y) < K then A20: y in dom f by FUNCT_1:11; A21: ((proj (i,n)) * f) . y = (proj (i,n)) . (f . y) by A19, FUNCT_1:12 .= (proj (i,n)) . (f /. y) by A20, PARTFUN1:def_6 ; ( 1 <= i & i <= n ) by A18, FINSEQ_1:1; then A22: |.((proj (i,n)) . (f /. y)).| <= |.(f /. y).| by PDIFF_8:5; A23: y in dom |.f.| by A20, NFCONT_4:def_2; then abs (|.f.| . y) < K by A17; then abs (|.f.| /. y) < K by A23, PARTFUN1:def_6; then abs |.(f /. y).| < K by A23, NFCONT_4:def_2; then |.(f /. y).| < K by ABSVALUE:def_1; hence abs (((proj (i,n)) * f) . y) < K by A21, A22, XXREAL_0:2; ::_thesis: verum end; hence (proj (i,n)) * f is bounded by COMSEQ_2:def_3; ::_thesis: verum end; Lm6: for n being Element of NAT for E being Element of REAL n for p being FinSequence of REAL n st ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds E = Sum p proof let n be Element of NAT ; ::_thesis: for E being Element of REAL n for p being FinSequence of REAL n st ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds E = Sum p let E be Element of REAL n; ::_thesis: for p being FinSequence of REAL n st ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds E = Sum p defpred S1[ Element of NAT ] means for p being FinSequence of REAL n for r being Element of REAL n st len p = $1 & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds r = Sum p; A1: S1[ 0 ] proof let p be FinSequence of REAL n; ::_thesis: for r being Element of REAL n st len p = 0 & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds r = Sum p let r be Element of REAL n; ::_thesis: ( len p = 0 & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) implies r = Sum p ) assume A2: ( len p = 0 & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) ) ; ::_thesis: r = Sum p A3: p = {} by A2; len r = n by CARD_1:def_7; then A4: dom r = Seg n by FINSEQ_1:def_3; A5: dom ((Seg n) --> 0) = Seg n by FUNCOP_1:13; A6: now__::_thesis:_for_x_being_set_st_x_in_dom_r_holds_ r_._x_=_((Seg_n)_-->_0)_._x let x be set ; ::_thesis: ( x in dom r implies r . x = ((Seg n) --> 0) . x ) assume A7: x in dom r ; ::_thesis: r . x = ((Seg n) --> 0) . x then reconsider i = x as Element of NAT ; set P = proj (i,n); consider Pi being FinSequence of REAL such that A8: ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) by A2, A4, A7; r . x = 0 by A3, A8, RVSUM_1:72; hence r . x = ((Seg n) --> 0) . x by A4, A7, FUNCOP_1:7; ::_thesis: verum end; Sum p = 0* n by A2, EUCLID_7:def_11; hence r = Sum p by A6, A4, A5, FUNCT_1:2; ::_thesis: verum end; A9: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A10: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_p_being_FinSequence_of_REAL_n for_r_being_Element_of_REAL_n_st_len_p_=_k_+_1_&_(_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ ex_Pi_being_FinSequence_of_REAL_st_ (_Pi_=_(proj_(i,n))_*_p_&_r_._i_=_Sum_Pi_)_)_holds_ r_=_Sum_p let p be FinSequence of REAL n; ::_thesis: for r being Element of REAL n st len p = k + 1 & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds r = Sum p let r be Element of REAL n; ::_thesis: ( len p = k + 1 & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) implies r = Sum p ) assume A11: ( len p = k + 1 & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) ) ; ::_thesis: r = Sum p set p1 = p | k; k + 1 in Seg (k + 1) by FINSEQ_1:4; then k + 1 in dom p by A11, FINSEQ_1:def_3; then p . (k + 1) in rng p by FUNCT_1:3; then reconsider pk1 = p . (k + 1) as Element of REAL n ; defpred S2[ Nat, set ] means ex P1i being FinSequence of REAL st ( P1i = (proj ($1,n)) * (p | k) & $2 = Sum P1i ); A12: for i being Nat st i in Seg n holds ex r being Element of REAL st S2[i,r] proof let i be Nat; ::_thesis: ( i in Seg n implies ex r being Element of REAL st S2[i,r] ) assume i in Seg n ; ::_thesis: ex r being Element of REAL st S2[i,r] take Sum ((proj (i,n)) * (p | k)) ; ::_thesis: S2[i, Sum ((proj (i,n)) * (p | k))] thus S2[i, Sum ((proj (i,n)) * (p | k))] ; ::_thesis: verum end; consider r1 being FinSequence of REAL such that A13: ( dom r1 = Seg n & ( for i being Nat st i in Seg n holds S2[i,r1 . i] ) ) from FINSEQ_1:sch_5(A12); len r1 = n by A13, FINSEQ_1:def_3; then reconsider r1 = r1 as Element of REAL n by FINSEQ_2:92; A14: for i being Element of NAT st i in Seg n holds ex P1i being FinSequence of REAL st ( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by A13; A15: k <= len p by A11, NAT_1:16; then A16: len (p | k) = k by FINSEQ_1:59; A17: len r = n by CARD_1:def_7; A18: len (r1 + pk1) = n by CARD_1:def_7; now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_n_holds_ r_._i_=_(r1_+_pk1)_._i let i be Nat; ::_thesis: ( 1 <= i & i <= n implies r . i = (r1 + pk1) . i ) set P = proj (i,n); assume ( 1 <= i & i <= n ) ; ::_thesis: r . i = (r1 + pk1) . i then A19: i in Seg n by FINSEQ_1:1; consider Pi being FinSequence of REAL such that A20: ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) by A19, A11; consider P1i being FinSequence of REAL such that A21: ( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by A19, A13; A22: dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then A23: rng p c= dom (proj (i,n)) ; A24: dom Pi = dom p by A23, A20, RELAT_1:27 .= Seg (len p) by FINSEQ_1:def_3 ; A25: len p = (len (p | k)) + (len <*(pk1 . i)*>) by A11, A16, FINSEQ_1:40; A26: rng (p | k) c= dom (proj (i,n)) by A22; A27: dom P1i = dom (p | k) by A26, A21, RELAT_1:27 .= Seg (len (p | k)) by FINSEQ_1:def_3 ; then A28: len P1i = len (p | k) by FINSEQ_1:def_3; A29: dom Pi = Seg ((len P1i) + (len <*(pk1 . i)*>)) by A24, A25, A27, FINSEQ_1:def_3; len (p | k) <= len p by A15, FINSEQ_1:59; then A30: Seg (len (p | k)) c= Seg (len p) by FINSEQ_1:5; A31: for k being Nat st k in dom P1i holds Pi . k = P1i . k proof let k be Nat; ::_thesis: ( k in dom P1i implies Pi . k = P1i . k ) assume A32: k in dom P1i ; ::_thesis: Pi . k = P1i . k then A33: k in dom (p | k) by A27, FINSEQ_1:def_3; thus P1i . k = (proj (i,n)) . ((p | k) . k) by A21, A32, FUNCT_1:12 .= (proj (i,n)) . (p . k) by A33, FUNCT_1:47 .= Pi . k by A20, A32, A24, A27, A30, FUNCT_1:12 ; ::_thesis: verum end; for k being Nat st k in dom <*(pk1 . i)*> holds Pi . ((len P1i) + k) = <*(pk1 . i)*> . k proof let j be Nat; ::_thesis: ( j in dom <*(pk1 . i)*> implies Pi . ((len P1i) + j) = <*(pk1 . i)*> . j ) assume j in dom <*(pk1 . i)*> ; ::_thesis: Pi . ((len P1i) + j) = <*(pk1 . i)*> . j then j in Seg (len <*(pk1 . i)*>) by FINSEQ_1:def_3; then j in Seg 1 by FINSEQ_1:40; then A34: j = 1 by FINSEQ_1:2, TARSKI:def_1; hence Pi . ((len P1i) + j) = (proj (i,n)) . (p . (k + 1)) by A20, A24, A11, A28, A16, FINSEQ_1:4, FUNCT_1:12 .= pk1 . i by PDIFF_1:def_1 .= <*(pk1 . i)*> . j by A34, FINSEQ_1:40 ; ::_thesis: verum end; then Pi = P1i ^ <*(pk1 . i)*> by A31, A29, FINSEQ_1:def_7; hence r . i = (r1 . i) + (pk1 . i) by A20, A21, RVSUM_1:74 .= (r1 + pk1) . i by RVSUM_1:11 ; ::_thesis: verum end; then A35: r = r1 + pk1 by A17, A18, FINSEQ_1:14; ex v being Element of REAL n st ( v = p . (len p) & Sum p = (Sum (p | k)) + v ) by A16, A11, PDIFF_6:15; hence r = Sum p by A11, A35, A10, A14, A16; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A36: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A9); let p be FinSequence of REAL n; ::_thesis: ( ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) implies E = Sum p ) assume A37: for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ; ::_thesis: E = Sum p len p = len p ; hence E = Sum p by A37, A36; ::_thesis: verum end; Lm7: for n being Element of NAT for E being Element of REAL n for p being FinSequence of REAL n for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds |.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds |.E.| <= Sum q proof let n be Element of NAT ; ::_thesis: for E being Element of REAL n for p being FinSequence of REAL n for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds |.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds |.E.| <= Sum q let E be Element of REAL n; ::_thesis: for p being FinSequence of REAL n for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds |.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds |.E.| <= Sum q let p be FinSequence of REAL n; ::_thesis: for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds |.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds |.E.| <= Sum q let q be FinSequence of REAL ; ::_thesis: ( len p = len q & ( for j being Nat st j in dom p holds |.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) implies |.E.| <= Sum q ) assume A1: ( len p = len q & ( for j being Nat st j in dom p holds |.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) ) ; ::_thesis: |.E.| <= Sum q then A2: E = Sum p by Lm6; defpred S1[ Nat, set ] means ex v being Element of REAL n st ( v = p . $1 & $2 = |.v.| ); A3: for i being Nat st i in Seg (len p) holds ex x being Element of REAL st S1[i,x] proof let i be Nat; ::_thesis: ( i in Seg (len p) implies ex x being Element of REAL st S1[i,x] ) assume i in Seg (len p) ; ::_thesis: ex x being Element of REAL st S1[i,x] then A4: i in dom p by FINSEQ_1:def_3; take |.(p /. i).| ; ::_thesis: S1[i,|.(p /. i).|] thus S1[i,|.(p /. i).|] by A4, PARTFUN1:def_6; ::_thesis: verum end; consider u being FinSequence of REAL such that A5: ( dom u = Seg (len p) & ( for i being Nat st i in Seg (len p) holds S1[i,u . i] ) ) from FINSEQ_1:sch_5(A3); A6: for i being Element of NAT st i in dom p holds ex v being Element of REAL n st ( v = p . i & u . i = |.v.| ) proof let i be Element of NAT ; ::_thesis: ( i in dom p implies ex v being Element of REAL n st ( v = p . i & u . i = |.v.| ) ) assume i in dom p ; ::_thesis: ex v being Element of REAL n st ( v = p . i & u . i = |.v.| ) then i in Seg (len p) by FINSEQ_1:def_3; hence ex v being Element of REAL n st ( v = p . i & u . i = |.v.| ) by A5; ::_thesis: verum end; A7: len u = len p by A5, FINSEQ_1:def_3; then A8: |.(Sum p).| <= Sum u by A6, PDIFF_6:17; set i = len p; reconsider uu = u as Element of (len p) -tuples_on REAL by A7, FINSEQ_2:92; reconsider qq = q as Element of (len p) -tuples_on REAL by A1, FINSEQ_2:92; now__::_thesis:_for_j_being_Nat_st_j_in_Seg_(len_p)_holds_ uu_._j_<=_qq_._j let j be Nat; ::_thesis: ( j in Seg (len p) implies uu . j <= qq . j ) assume A9: j in Seg (len p) ; ::_thesis: uu . j <= qq . j then A10: j in dom p by FINSEQ_1:def_3; then A11: |.(p /. j).| <= q /. j by A1; j in dom q by A9, A1, FINSEQ_1:def_3; then A12: q /. j = q . j by PARTFUN1:def_6; ex v being Element of REAL n st ( v = p . j & u . j = |.v.| ) by A6, A10; hence uu . j <= qq . j by A11, A12, A10, PARTFUN1:def_6; ::_thesis: verum end; then Sum uu <= Sum qq by RVSUM_1:82; hence |.E.| <= Sum q by A2, A8, XXREAL_0:2; ::_thesis: verum end; Lm8: for A being non empty closed_interval Subset of REAL for n being non empty Element of NAT for h being Function of A,(REAL n) for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds |.(integral h).| <= integral f proof let A be non empty closed_interval Subset of REAL; ::_thesis: for n being non empty Element of NAT for h being Function of A,(REAL n) for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds |.(integral h).| <= integral f let n be non empty Element of NAT ; ::_thesis: for h being Function of A,(REAL n) for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds |.(integral h).| <= integral f let h be Function of A,(REAL n); ::_thesis: for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds |.(integral h).| <= integral f let f be Function of A,REAL; ::_thesis: ( h is bounded & h is integrable & f = |.h.| & f is integrable implies |.(integral h).| <= integral f ) assume A1: ( h is bounded & h is integrable & f = |.h.| & f is integrable ) ; ::_thesis: |.(integral h).| <= integral f then A2: f is bounded by Th14; consider T being DivSequence of A such that A3: ( delta T is convergent & lim (delta T) = 0 ) by INTEGRA4:11; set S = the middle_volume_Sequence of h,T; A4: dom f = dom h by A1, NFCONT_4:def_2; defpred S1[ Element of NAT , set ] means ex p being FinSequence of REAL st ( p = $2 & len p = len (T . $1) & ( for i being Nat st i in dom (T . $1) holds ( p . i in dom (h | (divset ((T . $1),i))) & ex z being Element of REAL n st ( z = (h | (divset ((T . $1),i))) . (p . i) & ( the middle_volume_Sequence of h,T . $1) . i = (vol (divset ((T . $1),i))) * z ) ) ) ); A5: for k being Element of NAT ex p being Element of REAL * st S1[k,p] proof let k be Element of NAT ; ::_thesis: ex p being Element of REAL * st S1[k,p] defpred S2[ Nat, set ] means ( $2 in dom (h | (divset ((T . k),$1))) & ex c being Element of REAL n st ( c = (h | (divset ((T . k),$1))) . $2 & ( the middle_volume_Sequence of h,T . k) . $1 = (vol (divset ((T . k),$1))) * c ) ); A6: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3; A7: for i being Nat st i in Seg (len (T . k)) holds ex x being Element of REAL st S2[i,x] proof let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S2[i,x] ) assume i in Seg (len (T . k)) ; ::_thesis: ex x being Element of REAL st S2[i,x] then i in dom (T . k) by FINSEQ_1:def_3; then consider c being Element of REAL n such that A8: ( c in rng (h | (divset ((T . k),i))) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * c ) by INTEGR15:def_5; consider x being set such that A9: ( x in dom (h | (divset ((T . k),i))) & c = (h | (divset ((T . k),i))) . x ) by A8, FUNCT_1:def_3; ( x in dom h & x in divset ((T . k),i) ) by A9, RELAT_1:57; then reconsider x = x as Element of REAL ; take x ; ::_thesis: S2[i,x] thus S2[i,x] by A8, A9; ::_thesis: verum end; consider p being FinSequence of REAL such that A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds S2[i,p . i] ) ) from FINSEQ_1:sch_5(A7); take p ; ::_thesis: ( p is Element of REAL * & S1[k,p] ) len p = len (T . k) by A10, FINSEQ_1:def_3; hence ( p is Element of REAL * & S1[k,p] ) by A10, A6, FINSEQ_1:def_11; ::_thesis: verum end; consider F being Function of NAT,(REAL *) such that A11: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A5); defpred S2[ Element of NAT , set ] means ex q being middle_volume of f,T . $1 st ( q = $2 & ( for i being Nat st i in dom (T . $1) holds ex z being Element of REAL st ( (F . $1) . i in dom (f | (divset ((T . $1),i))) & z = (f | (divset ((T . $1),i))) . ((F . $1) . i) & q . i = (vol (divset ((T . $1),i))) * z ) ) ); A12: for k being Element of NAT ex y being Element of REAL * st S2[k,y] proof let k be Element of NAT ; ::_thesis: ex y being Element of REAL * st S2[k,y] defpred S3[ Nat, set ] means ex c being Element of REAL st ( (F . k) . $1 in dom (f | (divset ((T . k),$1))) & c = (f | (divset ((T . k),$1))) . ((F . k) . $1) & $2 = (vol (divset ((T . k),$1))) * c ); A13: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3; A14: for i being Nat st i in Seg (len (T . k)) holds ex x being Element of REAL st S3[i,x] proof let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S3[i,x] ) assume i in Seg (len (T . k)) ; ::_thesis: ex x being Element of REAL st S3[i,x] then A15: i in dom (T . k) by FINSEQ_1:def_3; consider p being FinSequence of REAL such that A16: ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds ( p . i in dom (h | (divset ((T . k),i))) & ex z being Element of REAL n st ( z = (h | (divset ((T . k),i))) . (p . i) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11; p . i in dom (h | (divset ((T . k),i))) by A15, A16; then ( p . i in dom h & p . i in divset ((T . k),i) ) by RELAT_1:57; then A17: (F . k) . i in dom (f | (divset ((T . k),i))) by A16, A4, RELAT_1:57; (vol (divset ((T . k),i))) * ((f | (divset ((T . k),i))) . (p . i)) is Element of REAL ; hence ex x being Element of REAL st S3[i,x] by A16, A17; ::_thesis: verum end; consider q being FinSequence of REAL such that A18: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds S3[i,q . i] ) ) from FINSEQ_1:sch_5(A14); A19: len q = len (T . k) by A18, FINSEQ_1:def_3; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(T_._k)_holds_ ex_c_being_Element_of_REAL_st_ (_c_in_rng_(f_|_(divset_((T_._k),i)))_&_q_._i_=_c_*_(vol_(divset_((T_._k),i)))_) let i be Nat; ::_thesis: ( i in dom (T . k) implies ex c being Element of REAL st ( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) ) ) assume i in dom (T . k) ; ::_thesis: ex c being Element of REAL st ( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) ) then i in Seg (len (T . k)) by FINSEQ_1:def_3; then consider c being Element of REAL such that A20: ( (F . k) . i in dom (f | (divset ((T . k),i))) & c = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * c ) by A18; thus ex c being Element of REAL st ( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) ) by A20, FUNCT_1:3; ::_thesis: verum end; then reconsider q = q as middle_volume of f,T . k by A19, INTEGR15:def_1; q is Element of REAL * by FINSEQ_1:def_11; hence ex y being Element of REAL * st S2[k,y] by A13, A18; ::_thesis: verum end; consider Sf being Function of NAT,(REAL *) such that A21: for x being Element of NAT holds S2[x,Sf . x] from FUNCT_2:sch_3(A12); now__::_thesis:_for_k_being_Element_of_NAT_holds_Sf_._k_is_middle_volume_of_f,T_._k let k be Element of NAT ; ::_thesis: Sf . k is middle_volume of f,T . k ex q being middle_volume of f,T . k st ( q = Sf . k & ( for i being Nat st i in dom (T . k) holds ex z being Element of REAL st ( (F . k) . i in dom (f | (divset ((T . k),i))) & z = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A21; hence Sf . k is middle_volume of f,T . k ; ::_thesis: verum end; then reconsider Sf = Sf as middle_volume_Sequence of f,T by INTEGR15:def_3; A22: ( middle_sum (f,Sf) is convergent & lim (middle_sum (f,Sf)) = integral f ) by A1, A2, A3, INTEGR15:9; A23: ( middle_sum (h, the middle_volume_Sequence of h,T) is convergent & lim (middle_sum (h, the middle_volume_Sequence of h,T)) = integral h ) by A1, A3, INTEGR15:11; A24: for k being Element of NAT holds ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k proof let k be Element of NAT ; ::_thesis: ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k A25: (middle_sum (f,Sf)) . k = middle_sum (f,(Sf . k)) by INTEGR15:def_4 .= Sum (Sf . k) ; A26: (middle_sum (h, the middle_volume_Sequence of h,T)) . k = middle_sum (h,( the middle_volume_Sequence of h,T . k)) by INTEGR15:def_8; A27: for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * ( the middle_volume_Sequence of h,T . k) & (middle_sum (h,( the middle_volume_Sequence of h,T . k))) . i = Sum Pi ) by INTEGR15:def_6; A28: ex p being FinSequence of REAL st ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds ( p . i in dom (h | (divset ((T . k),i))) & ex z being Element of REAL n st ( z = (h | (divset ((T . k),i))) . (p . i) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11; A29: ex q being middle_volume of f,T . k st ( q = Sf . k & ( for i being Nat st i in dom (T . k) holds ex z being Element of REAL st ( (F . k) . i in dom (f | (divset ((T . k),i))) & z = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A21; A30: len (Sf . k) = len (T . k) by INTEGR15:def_1; A31: len ( the middle_volume_Sequence of h,T . k) = len (T . k) by INTEGR15:def_5; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(_the_middle_volume_Sequence_of_h,T_._k)_holds_ |.((_the_middle_volume_Sequence_of_h,T_._k)_/._i).|_<=_(Sf_._k)_/._i let i be Nat; ::_thesis: ( i in dom ( the middle_volume_Sequence of h,T . k) implies |.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i ) assume A32: i in dom ( the middle_volume_Sequence of h,T . k) ; ::_thesis: |.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i then A33: i in Seg (len (T . k)) by A31, FINSEQ_1:def_3; then A34: i in dom (T . k) by FINSEQ_1:def_3; A35: i in dom (Sf . k) by A30, A33, FINSEQ_1:def_3; A36: (F . k) . i in dom (h | (divset ((T . k),i))) by A34, A28; consider z being Element of REAL n such that A37: ( z = (h | (divset ((T . k),i))) . ((F . k) . i) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) by A28, A34; consider w being Element of REAL such that A38: ( (F . k) . i in dom (f | (divset ((T . k),i))) & w = (f | (divset ((T . k),i))) . ((F . k) . i) & (Sf . k) . i = (vol (divset ((T . k),i))) * w ) by A29, A34; A39: ( the middle_volume_Sequence of h,T . k) /. i = ( the middle_volume_Sequence of h,T . k) . i by A32, PARTFUN1:def_6; A40: 0 <= vol (divset ((T . k),i)) by INTEGRA1:9; A41: |.(( the middle_volume_Sequence of h,T . k) /. i).| = (abs (vol (divset ((T . k),i)))) * |.z.| by A37, A39, EUCLID:11 .= (vol (divset ((T . k),i))) * |.z.| by A40, ABSVALUE:def_1 ; A42: dom (h | (divset ((T . k),i))) c= dom h by RELAT_1:60; A43: (h | (divset ((T . k),i))) . ((F . k) . i) = h . ((F . k) . i) by A36, FUNCT_1:47 .= h /. ((F . k) . i) by A42, A36, PARTFUN1:def_6 ; A44: dom (f | (divset ((T . k),i))) c= dom f by RELAT_1:60; (f | (divset ((T . k),i))) . ((F . k) . i) = f . ((F . k) . i) by A38, FUNCT_1:47 .= |.h.| /. ((F . k) . i) by A44, A1, A38, PARTFUN1:def_6 .= |.(h /. ((F . k) . i)).| by A44, A1, A38, NFCONT_4:def_2 ; hence |.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i by A41, A43, A38, A37, A35, PARTFUN1:def_6; ::_thesis: verum end; then |.(middle_sum (h,( the middle_volume_Sequence of h,T . k))).| <= Sum (Sf . k) by Lm7, A27, A30, A31; hence ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k by A25, A26, REAL_NS1:1; ::_thesis: verum end; A45: now__::_thesis:_for_i_being_Element_of_NAT_holds_||.(middle_sum_(h,_the_middle_volume_Sequence_of_h,T)).||_._i_<=_(middle_sum_(f,Sf))_._i let i be Element of NAT ; ::_thesis: ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i <= (middle_sum (f,Sf)) . i ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i = ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . i).|| by NORMSP_0:def_4; hence ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i <= (middle_sum (f,Sf)) . i by A24; ::_thesis: verum end; ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| is convergent by A1, A3, INTEGR15:11, NORMSP_1:23; then lim ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| <= lim (middle_sum (f,Sf)) by A45, A22, SEQ_2:18; then ||.(lim (middle_sum (h, the middle_volume_Sequence of h,T))).|| <= lim (middle_sum (f,Sf)) by A23, LOPBAN_1:41; hence |.(integral h).| <= integral f by A22, A1, A3, INTEGR15:11, REAL_NS1:1; ::_thesis: verum end; Lm9: for n being Element of NAT for A being non empty closed_interval Subset of REAL for h being PartFunc of REAL,(REAL n) st A c= dom h holds h | A is Function of A,(REAL n) by Lm3; theorem :: INTEGR19:15 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) st f is bounded & A c= dom f holds f | A is bounded proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) st f is bounded & A c= dom f holds f | A is bounded let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is bounded & A c= dom f holds f | A is bounded let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is bounded & A c= dom f implies f | A is bounded ) assume A1: ( f is bounded & A c= dom f ) ; ::_thesis: f | A is bounded let i be Element of NAT ; :: according to INTEGR15:def_15 ::_thesis: ( not i in Seg n or (proj (i,n)) * (f | A) is bounded ) set P = proj (i,n); assume i in Seg n ; ::_thesis: (proj (i,n)) * (f | A) is bounded then (proj (i,n)) * f is bounded by A1, INTEGR15:def_15; then consider r being real number such that A2: for c being set st c in dom ((proj (i,n)) * f) holds abs (((proj (i,n)) * f) . c) <= r by RFUNCT_1:72; now__::_thesis:_for_c_being_set_st_c_in_A_/\_(dom_((proj_(i,n))_*_f))_holds_ abs_(((proj_(i,n))_*_f)_._c)_<=_r let c be set ; ::_thesis: ( c in A /\ (dom ((proj (i,n)) * f)) implies abs (((proj (i,n)) * f) . c) <= r ) assume c in A /\ (dom ((proj (i,n)) * f)) ; ::_thesis: abs (((proj (i,n)) * f) . c) <= r then c in dom ((proj (i,n)) * f) by XBOOLE_0:def_4; hence abs (((proj (i,n)) * f) . c) <= r by A2; ::_thesis: verum end; then ((proj (i,n)) * f) | A is bounded by RFUNCT_1:73; hence (proj (i,n)) * (f | A) is bounded by RELAT_1:83; ::_thesis: verum end; theorem Th16: :: INTEGR19:16 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for g being Function of A,(REAL n) st f is bounded & f = g holds g is bounded proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for g being Function of A,(REAL n) st f is bounded & f = g holds g is bounded let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) for g being Function of A,(REAL n) st f is bounded & f = g holds g is bounded let f be PartFunc of REAL,(REAL n); ::_thesis: for g being Function of A,(REAL n) st f is bounded & f = g holds g is bounded let g be Function of A,(REAL n); ::_thesis: ( f is bounded & f = g implies g is bounded ) assume A1: ( f is bounded & f = g ) ; ::_thesis: g is bounded let i be Element of NAT ; :: according to INTEGR15:def_12 ::_thesis: ( not i in Seg n or (proj (i,n)) * g is bounded ) thus ( not i in Seg n or (proj (i,n)) * g is bounded ) by A1, INTEGR15:def_15; ::_thesis: verum end; theorem Th17: :: INTEGR19:17 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for g being Function of A,(REAL n) st f = g holds |.f.| = |.g.| proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for g being Function of A,(REAL n) st f = g holds |.f.| = |.g.| let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) for g being Function of A,(REAL n) st f = g holds |.f.| = |.g.| let f be PartFunc of REAL,(REAL n); ::_thesis: for g being Function of A,(REAL n) st f = g holds |.f.| = |.g.| let g be Function of A,(REAL n); ::_thesis: ( f = g implies |.f.| = |.g.| ) assume A1: f = g ; ::_thesis: |.f.| = |.g.| A2: dom |.f.| = dom f by NFCONT_4:def_2 .= dom |.g.| by A1, NFCONT_4:def_2 ; now__::_thesis:_for_x_being_set_st_x_in_dom_|.f.|_holds_ |.f.|_._x_=_|.g.|_._x let x be set ; ::_thesis: ( x in dom |.f.| implies |.f.| . x = |.g.| . x ) assume A3: x in dom |.f.| ; ::_thesis: |.f.| . x = |.g.| . x thus |.f.| . x = |.f.| /. x by A3, PARTFUN1:def_6 .= |.(f /. x).| by A3, NFCONT_4:def_2 .= |.g.| /. x by A1, A2, A3, NFCONT_4:def_2 .= |.g.| . x by A2, A3, PARTFUN1:def_6 ; ::_thesis: verum end; hence |.f.| = |.g.| by A2, FUNCT_1:2; ::_thesis: verum end; theorem Th18: :: INTEGR19:18 for n being Element of NAT for A being non empty closed_interval Subset of REAL for h being PartFunc of REAL,(REAL n) st A c= dom h holds |.(h | A).| = |.h.| | A proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for h being PartFunc of REAL,(REAL n) st A c= dom h holds |.(h | A).| = |.h.| | A let A be non empty closed_interval Subset of REAL; ::_thesis: for h being PartFunc of REAL,(REAL n) st A c= dom h holds |.(h | A).| = |.h.| | A let h be PartFunc of REAL,(REAL n); ::_thesis: ( A c= dom h implies |.(h | A).| = |.h.| | A ) assume A1: A c= dom h ; ::_thesis: |.(h | A).| = |.h.| | A A2: dom (h | A) = A by A1, RELAT_1:62; A3: dom (|.h.| | A) = (dom |.h.|) /\ A by RELAT_1:61 .= (dom h) /\ A by NFCONT_4:def_2 .= A by A1, XBOOLE_1:28 ; A4: dom |.(h | A).| = dom (|.h.| | A) by A3, A2, NFCONT_4:def_2; now__::_thesis:_for_x_being_set_st_x_in_dom_(|.h.|_|_A)_holds_ (|.h.|_|_A)_._x_=_|.(h_|_A).|_._x let x be set ; ::_thesis: ( x in dom (|.h.| | A) implies (|.h.| | A) . x = |.(h | A).| . x ) assume A5: x in dom (|.h.| | A) ; ::_thesis: (|.h.| | A) . x = |.(h | A).| . x then A6: x in (dom |.h.|) /\ A by RELAT_1:61; then A7: x in (dom h) /\ A by NFCONT_4:def_2; then A8: x in dom (h | A) by RELAT_1:61; A9: x in dom |.h.| by A6, XBOOLE_0:def_4; A10: x in dom h by A7, XBOOLE_0:def_4; A11: h /. x = h . x by A10, PARTFUN1:def_6 .= (h | A) . x by A8, FUNCT_1:47 .= (h | A) /. x by A8, PARTFUN1:def_6 ; thus (|.h.| | A) . x = |.h.| . x by A6, FUNCT_1:48 .= |.h.| /. x by A9, PARTFUN1:def_6 .= |.(h /. x).| by A9, NFCONT_4:def_2 .= |.(h | A).| /. x by A11, A4, A5, NFCONT_4:def_2 .= |.(h | A).| . x by A4, A5, PARTFUN1:def_6 ; ::_thesis: verum end; hence |.(h | A).| = |.h.| | A by A4, FUNCT_1:2; ::_thesis: verum end; theorem Th19: :: INTEGR19:19 for A being non empty closed_interval Subset of REAL for n being non empty Element of NAT for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded holds |.h.| | A is bounded proof let A be non empty closed_interval Subset of REAL; ::_thesis: for n being non empty Element of NAT for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded holds |.h.| | A is bounded let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded holds |.h.| | A is bounded let h be PartFunc of REAL,(REAL n); ::_thesis: ( A c= dom h & h | A is bounded implies |.h.| | A is bounded ) assume A1: ( A c= dom h & h | A is bounded ) ; ::_thesis: |.h.| | A is bounded A2: |.(h | A).| = |.h.| | A by Th18, A1; reconsider g = h | A as Function of A,(REAL n) by A1, Lm9; g is bounded by Th16, A1; then |.g.| is bounded by Th14; hence |.h.| | A is bounded by A2, Th17; ::_thesis: verum end; theorem Th20: :: INTEGR19:20 for A being non empty closed_interval Subset of REAL for n being non empty Element of NAT for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A holds |.(integral (h,A)).| <= integral (|.h.|,A) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for n being non empty Element of NAT for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A holds |.(integral (h,A)).| <= integral (|.h.|,A) let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A holds |.(integral (h,A)).| <= integral (|.h.|,A) let h be PartFunc of REAL,(REAL n); ::_thesis: ( A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A implies |.(integral (h,A)).| <= integral (|.h.|,A) ) assume A1: ( A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A ) ; ::_thesis: |.(integral (h,A)).| <= integral (|.h.|,A) set f = |.h.|; reconsider hA = h | A as Function of A,(REAL n) by A1, Lm9; A2: integral (h,A) = integral hA by INTEGR15:14; A c= dom |.h.| by A1, NFCONT_4:def_2; then reconsider fA = |.h.| | A as Function of A,REAL by Lm5; A3: fA is integrable by A1, INTEGRA5:def_1; A4: hA is integrable by A1, INTEGR15:13; |.hA.| = |.(h | A).| by Th17 .= |.h.| | A by Th18, A1 ; hence |.(integral (h,A)).| <= integral (|.h.|,A) by A2, A3, A4, A1, Th16, Lm8; ::_thesis: verum end; theorem Th21: :: INTEGR19:21 for a, b being real number for n being non empty Element of NAT for h being PartFunc of REAL,(REAL n) st a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded holds |.(integral (h,a,b)).| <= integral (|.h.|,a,b) proof let a, b be real number ; ::_thesis: for n being non empty Element of NAT for h being PartFunc of REAL,(REAL n) st a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded holds |.(integral (h,a,b)).| <= integral (|.h.|,a,b) let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL n) st a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded holds |.(integral (h,a,b)).| <= integral (|.h.|,a,b) let h be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded implies |.(integral (h,a,b)).| <= integral (|.h.|,a,b) ) assume A1: ( a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded ) ; ::_thesis: |.(integral (h,a,b)).| <= integral (|.h.|,a,b) A2: ( a is Real & b is Real ) by XREAL_0:def_1; ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A3: integral (h,a,b) = integral (h,['a,b']) by A2, INTEGR15:19; integral (|.h.|,a,b) = integral (|.h.|,['a,b']) by A1, INTEGRA5:def_4; hence |.(integral (h,a,b)).| <= integral (|.h.|,a,b) by Th20, A1, A3; ::_thesis: verum end; Lm10: for a, b, c, d being real number for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( f is_integrable_on ['c,d'] & |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) proof let a, b, c, d be real number ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( f is_integrable_on ['c,d'] & |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( f is_integrable_on ['c,d'] & |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies ( f is_integrable_on ['c,d'] & |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) ) assume that A1: a <= b and A2: c <= d and A3: ( f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f ) and A4: ( c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( f is_integrable_on ['c,d'] & |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A5: ( a <= c & d <= b ) by A4, XXREAL_1:1; then A6: f | ['c,d'] is bounded by A2, A3, Th9; A7: ( ['c,d'] c= dom f & f is_integrable_on ['c,d'] ) by A2, A3, A5, Th9, Th2; A8: ['a,b'] c= dom |.f.| by A3, NFCONT_4:def_2; |.f.| | ['a,b'] is bounded by A3, Th19; then ( ['c,d'] c= dom |.f.| & |.f.| is_integrable_on ['c,d'] ) by A2, A3, A5, A8, INTEGRA6:18; hence ( f is_integrable_on ['c,d'] & |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) by A2, A6, A7, Th21, Th19; ::_thesis: verum end; theorem Th22: :: INTEGR19:22 for a, b, c, d being real number for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) proof let a, b, c, d be real number ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) ) assume A1: ( a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) A2: ( c is Real & d is Real ) by XREAL_0:def_1; percases ( not c <= d or c <= d ) ; supposeA3: not c <= d ; ::_thesis: ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) then A4: ['d,c'] = [.d,c.] by INTEGRA5:def_3; then integral (f,c,d) = - (integral (f,['d,c'])) by A2, INTEGR15:20; then integral (f,c,d) = - (integral (f,d,c)) by A2, A4, INTEGR15:19; then A5: |.(integral (f,c,d)).| = |.(integral (f,d,c)).| by EUCLID:10; ( d = min (c,d) & c = max (c,d) ) by A3, XXREAL_0:def_9, XXREAL_0:def_10; hence ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) by A1, A3, A5, Lm10; ::_thesis: verum end; supposeA6: c <= d ; ::_thesis: ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) then ( c = min (c,d) & d = max (c,d) ) by XXREAL_0:def_9, XXREAL_0:def_10; hence ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) by A1, A6, Lm10; ::_thesis: verum end; end; end; Lm11: for a, b, c, d being real number for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) proof let a, b, c, d be real number ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies ( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) ) assume that A1: a <= b and A2: c <= d and A3: ( f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) ( min (c,d) = c & max (c,d) = d ) by A2, XXREAL_0:def_9, XXREAL_0:def_10; hence ( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) by A1, A3, Th22; ::_thesis: verum end; Lm12: for a, b, c, d being real number for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds |.(integral (f,d,c)).| <= integral (|.f.|,c,d) proof let a, b, c, d be real number ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds |.(integral (f,d,c)).| <= integral (|.f.|,c,d) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds |.(integral (f,d,c)).| <= integral (|.f.|,c,d) let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies |.(integral (f,d,c)).| <= integral (|.f.|,c,d) ) assume that A1: a <= b and A2: c <= d and A3: ( f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] ) and A4: d in ['a,b'] ; ::_thesis: |.(integral (f,d,c)).| <= integral (|.f.|,c,d) A5: ( c is Real & d is Real ) by XREAL_0:def_1; ['c,d'] = [.c,d.] by A2, INTEGRA5:def_3; then A6: ( |.(integral (f,c,d)).| <= integral (|.f.|,c,d) & integral (f,c,d) = integral (f,['c,d']) ) by A1, A2, A3, A4, Lm11, INTEGR15:19; ['c,d'] = [.c,d.] by A2, INTEGRA5:def_3; then integral (f,d,c) = - (integral (f,['c,d'])) by A5, INTEGR15:20; hence |.(integral (f,d,c)).| <= integral (|.f.|,c,d) by A6, EUCLID:10; ::_thesis: verum end; theorem :: INTEGR19:23 for a, b, c, d being real number for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) & |.(integral (f,d,c)).| <= integral (|.f.|,c,d) ) by Lm11, Lm12; Lm13: for a, b, c, d, e being real number for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds |.(f /. x).| <= e ) holds |.(integral (f,c,d)).| <= e * (abs (d - c)) proof let a, b, c, d, e be real number ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds |.(f /. x).| <= e ) holds |.(integral (f,c,d)).| <= e * (abs (d - c)) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds |.(f /. x).| <= e ) holds |.(integral (f,c,d)).| <= e * (abs (d - c)) let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds |.(f /. x).| <= e ) implies |.(integral (f,c,d)).| <= e * (abs (d - c)) ) set A = ['(min (c,d)),(max (c,d))']; assume that A1: ( a <= b & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) and A2: for x being real number st x in ['(min (c,d)),(max (c,d))'] holds |.(f /. x).| <= e ; ::_thesis: |.(integral (f,c,d)).| <= e * (abs (d - c)) rng |.f.| c= REAL ; then A3: |.f.| is Function of (dom |.f.|),REAL by FUNCT_2:2; dom |.f.| = dom f by NFCONT_4:def_2; then A4: ['(min (c,d)),(max (c,d))'] c= dom |.f.| by A1, Th3; then reconsider g = |.f.| | ['(min (c,d)),(max (c,d))'] as Function of ['(min (c,d)),(max (c,d))'],REAL by A3, FUNCT_2:32; A5: vol ['(min (c,d)),(max (c,d))'] = abs (d - c) by INTEGRA6:6; |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] by A1, Th22; then A6: g is integrable by INTEGRA5:def_1; e is Real by XREAL_0:def_1; then consider h being Function of ['(min (c,d)),(max (c,d))'],REAL such that A7: rng h = {e} and A8: h | ['(min (c,d)),(max (c,d))'] is bounded by INTEGRA4:5; A9: now__::_thesis:_for_x_being_Real_st_x_in_['(min_(c,d)),(max_(c,d))']_holds_ g_._x_<=_h_._x let x be Real; ::_thesis: ( x in ['(min (c,d)),(max (c,d))'] implies g . x <= h . x ) assume A10: x in ['(min (c,d)),(max (c,d))'] ; ::_thesis: g . x <= h . x then g . x = |.f.| . x by FUNCT_1:49; then g . x = |.f.| /. x by A10, A4, PARTFUN1:def_6; then A11: g . x = |.(f /. x).| by A10, A4, NFCONT_4:def_2; h . x in {e} by A7, A10, FUNCT_2:4; then h . x = e by TARSKI:def_1; hence g . x <= h . x by A11, A2, A10; ::_thesis: verum end; A12: |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) by A1, Th22; ( min (c,d) <= c & c <= max (c,d) ) by XXREAL_0:17, XXREAL_0:25; then min (c,d) <= max (c,d) by XXREAL_0:2; then A13: integral (|.f.|,(min (c,d)),(max (c,d))) = integral (|.f.|,['(min (c,d)),(max (c,d))']) by INTEGRA5:def_4; |.f.| | ['(min (c,d)),(max (c,d))'] is bounded by A1, Th22; then A14: g | ['(min (c,d)),(max (c,d))'] is bounded ; e is Real by XREAL_0:def_1; then ( h is integrable & integral h = e * (vol ['(min (c,d)),(max (c,d))']) ) by A7, INTEGRA4:4; then integral (|.f.|,(min (c,d)),(max (c,d))) <= e * (abs (d - c)) by A13, A8, A9, A6, A14, A5, INTEGRA2:34; hence |.(integral (f,c,d)).| <= e * (abs (d - c)) by A12, XXREAL_0:2; ::_thesis: verum end; Lm14: for a, b, c, d, e being real number for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds |.(f /. x).| <= e ) holds |.(integral (f,c,d)).| <= e * (d - c) proof let a, b, c, d, e be real number ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds |.(f /. x).| <= e ) holds |.(integral (f,c,d)).| <= e * (d - c) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds |.(f /. x).| <= e ) holds |.(integral (f,c,d)).| <= e * (d - c) let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds |.(f /. x).| <= e ) implies |.(integral (f,c,d)).| <= e * (d - c) ) assume that A1: a <= b and A2: c <= d and A3: ( f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds |.(f /. x).| <= e ) ) ; ::_thesis: |.(integral (f,c,d)).| <= e * (d - c) 0 <= d - c by A2, XREAL_1:48; then A4: abs (d - c) = d - c by ABSVALUE:def_1; ( min (c,d) = c & max (c,d) = d ) by A2, XXREAL_0:def_9, XXREAL_0:def_10; hence |.(integral (f,c,d)).| <= e * (d - c) by A1, A3, A4, Lm13; ::_thesis: verum end; Lm15: for a, b, c, d, e being real number for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds |.(f /. x).| <= e ) holds |.(integral (f,d,c)).| <= e * (d - c) proof let a, b, c, d, e be real number ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds |.(f /. x).| <= e ) holds |.(integral (f,d,c)).| <= e * (d - c) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds |.(f /. x).| <= e ) holds |.(integral (f,d,c)).| <= e * (d - c) let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds |.(f /. x).| <= e ) implies |.(integral (f,d,c)).| <= e * (d - c) ) assume that A1: a <= b and A2: c <= d and A3: ( f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] ) and A4: d in ['a,b'] and A5: for x being real number st x in ['c,d'] holds |.(f /. x).| <= e ; ::_thesis: |.(integral (f,d,c)).| <= e * (d - c) ['c,d'] = [.c,d.] by A2, INTEGRA5:def_3; then A6: ( |.(integral (f,c,d)).| <= e * (d - c) & integral (f,c,d) = integral (f,['c,d']) ) by A1, A2, A3, A4, A5, Lm14, INTEGR15:19; A7: ( c is Real & d is Real ) by XREAL_0:def_1; ['c,d'] = [.c,d.] by A2, INTEGRA5:def_3; then integral (f,d,c) = - (integral (f,['c,d'])) by A7, INTEGR15:20; hence |.(integral (f,d,c)).| <= e * (d - c) by A6, EUCLID:10; ::_thesis: verum end; theorem :: INTEGR19:24 for a, b, c, d, e being real number for n being non empty Element of NAT for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds |.(f /. x).| <= e ) holds ( |.(integral (f,c,d)).| <= e * (d - c) & |.(integral (f,d,c)).| <= e * (d - c) ) by Lm14, Lm15; theorem Th25: :: INTEGR19:25 for n being Element of NAT for a, b, c, d, r being real number for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral ((r (#) f),c,d) = r * (integral (f,c,d)) proof let n be Element of NAT ; ::_thesis: for a, b, c, d, r being real number for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral ((r (#) f),c,d) = r * (integral (f,c,d)) let a, b, c, d, r be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral ((r (#) f),c,d) = r * (integral (f,c,d)) let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral ((r (#) f),c,d) = r * (integral (f,c,d)) ) assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((r (#) f),c,d) = r * (integral (f,c,d)) A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ integral_(((proj_(i,n))_*_(r_(#)_f)),c,d)_=_r_*_(integral_(((proj_(i,n))_*_f),c,d)) let i be Element of NAT ; ::_thesis: ( i in Seg n implies integral (((proj (i,n)) * (r (#) f)),c,d) = r * (integral (((proj (i,n)) * f),c,d)) ) set P = proj (i,n); assume A3: i in Seg n ; ::_thesis: integral (((proj (i,n)) * (r (#) f)),c,d) = r * (integral (((proj (i,n)) * f),c,d)) then A4: (proj (i,n)) * f is_integrable_on ['a,b'] by A1, INTEGR15:def_16; (proj (i,n)) * (f | ['a,b']) is bounded by A3, A1, INTEGR15:def_15; 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 A6: ['a,b'] c= dom ((proj (i,n)) * f) by A1, RELAT_1:27; r is Real by XREAL_0:def_1; then (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f) by INTEGR15:16; hence integral (((proj (i,n)) * (r (#) f)),c,d) = r * (integral (((proj (i,n)) * f),c,d)) by A4, A5, A6, A1, INTEGRA6:25; ::_thesis: verum end; A7: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(integral_((r_(#)_f),c,d))_holds_ (integral_((r_(#)_f),c,d))_._i_=_(r_*_(integral_(f,c,d)))_._i let i be Nat; ::_thesis: ( i in dom (integral ((r (#) f),c,d)) implies (integral ((r (#) f),c,d)) . i = (r * (integral (f,c,d))) . i ) assume i in dom (integral ((r (#) f),c,d)) ; ::_thesis: (integral ((r (#) f),c,d)) . i = (r * (integral (f,c,d))) . i then A8: i in Seg n by INTEGR15:def_18; set P = proj (i,n); thus (integral ((r (#) f),c,d)) . i = integral (((proj (i,n)) * (r (#) f)),c,d) by A8, INTEGR15:def_18 .= r * (integral (((proj (i,n)) * f),c,d)) by A8, A2 .= r * ((integral (f,c,d)) . i) by A8, INTEGR15:def_18 .= (r * (integral (f,c,d))) . i by RVSUM_1:44 ; ::_thesis: verum end; A9: Seg n = dom (integral ((r (#) f),c,d)) by INTEGR15:def_18; len (r * (integral (f,c,d))) = n by CARD_1:def_7; then Seg n = dom (r * (integral (f,c,d))) by FINSEQ_1:def_3; hence integral ((r (#) f),c,d) = r * (integral (f,c,d)) by A9, A7, FINSEQ_1:13; ::_thesis: verum end; theorem Th26: :: INTEGR19:26 for n being Element of NAT for a, b, c, d being real number for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral ((- f),c,d) = - (integral (f,c,d)) proof let n be Element of NAT ; ::_thesis: for a, b, c, d being real number for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral ((- f),c,d) = - (integral (f,c,d)) let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral ((- f),c,d) = - (integral (f,c,d)) let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral ((- f),c,d) = - (integral (f,c,d)) ) - f = (- 1) (#) f by NFCONT_4:7; hence ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral ((- f),c,d) = - (integral (f,c,d)) ) by Th25; ::_thesis: verum end; theorem Th27: :: INTEGR19:27 for n being Element of NAT for a, b, c, d being real number for f, g being PartFunc of REAL,(REAL n) st a <= 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 & c in ['a,b'] & d in ['a,b'] holds integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) proof let n be Element of NAT ; ::_thesis: for a, b, c, d being real number for f, g being PartFunc of REAL,(REAL n) st a <= 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 & c in ['a,b'] & d in ['a,b'] holds integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) let a, b, c, d be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL n) st a <= 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 & c in ['a,b'] & d in ['a,b'] holds integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) let f, g be PartFunc of REAL,(REAL n); ::_thesis: ( a <= 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 & c in ['a,b'] & d in ['a,b'] implies integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) ) assume A1: ( a <= 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 & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ integral_(((proj_(i,n))_*_(f_+_g)),c,d)_=_(integral_(((proj_(i,n))_*_f),c,d))_+_(integral_(((proj_(i,n))_*_g),c,d)) let i be Element of NAT ; ::_thesis: ( i in Seg n implies integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d)) ) set P = proj (i,n); assume A3: i in Seg n ; ::_thesis: integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d)) then A4: (proj (i,n)) * f is_integrable_on ['a,b'] by A1, INTEGR15:def_16; (proj (i,n)) * (f | ['a,b']) is bounded by A3, A1, INTEGR15:def_15; then A5: ((proj (i,n)) * f) | ['a,b'] is bounded by RELAT_1:83; A6: (proj (i,n)) * g is_integrable_on ['a,b'] by A3, A1, INTEGR15:def_16; (proj (i,n)) * (g | ['a,b']) is bounded by A3, A1, INTEGR15:def_15; then A7: ((proj (i,n)) * g) | ['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: ['a,b'] c= dom ((proj (i,n)) * f) by A1, RELAT_1:27; rng g c= dom (proj (i,n)) by A8; then A10: ['a,b'] c= dom ((proj (i,n)) * g) by A1, RELAT_1:27; A11: (proj (i,n)) * (f + g) = ((proj (i,n)) * f) + ((proj (i,n)) * g) by INTEGR15:15; thus integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d)) by A4, A5, A9, A6, A7, A10, A1, A11, INTEGRA6:24; ::_thesis: verum end; A12: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(integral_((f_+_g),c,d))_holds_ (integral_((f_+_g),c,d))_._i_=_((integral_(f,c,d))_+_(integral_(g,c,d)))_._i let i be Nat; ::_thesis: ( i in dom (integral ((f + g),c,d)) implies (integral ((f + g),c,d)) . i = ((integral (f,c,d)) + (integral (g,c,d))) . i ) assume i in dom (integral ((f + g),c,d)) ; ::_thesis: (integral ((f + g),c,d)) . i = ((integral (f,c,d)) + (integral (g,c,d))) . i then A13: i in Seg n by INTEGR15:def_18; set P = proj (i,n); thus (integral ((f + g),c,d)) . i = integral (((proj (i,n)) * (f + g)),c,d) by A13, INTEGR15:def_18 .= (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d)) by A13, A2 .= ((integral (f,c,d)) . i) + (integral (((proj (i,n)) * g),c,d)) by A13, INTEGR15:def_18 .= ((integral (f,c,d)) . i) + ((integral (g,c,d)) . i) by A13, INTEGR15:def_18 .= ((integral (f,c,d)) + (integral (g,c,d))) . i by RVSUM_1:11 ; ::_thesis: verum end; A14: Seg n = dom (integral ((f + g),c,d)) by INTEGR15:def_18; len ((integral (f,c,d)) + (integral (g,c,d))) = n by CARD_1:def_7; then Seg n = dom ((integral (f,c,d)) + (integral (g,c,d))) by FINSEQ_1:def_3; hence integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) by A14, A12, FINSEQ_1:13; ::_thesis: verum end; theorem Th28: :: INTEGR19:28 for n being Element of NAT for a, b, c, d being real number for f, g being PartFunc of REAL,(REAL n) st a <= 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 & c in ['a,b'] & d in ['a,b'] holds integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) proof let n be Element of NAT ; ::_thesis: for a, b, c, d being real number for f, g being PartFunc of REAL,(REAL n) st a <= 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 & c in ['a,b'] & d in ['a,b'] holds integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) let a, b, c, d be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL n) st a <= 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 & c in ['a,b'] & d in ['a,b'] holds integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) let f, g be PartFunc of REAL,(REAL n); ::_thesis: ( a <= 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 & c in ['a,b'] & d in ['a,b'] implies integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) assume A1: ( a <= 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 & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) A2: ( - g is_integrable_on ['a,b'] & (- g) | ['a,b'] is bounded ) by A1, Th12; A3: dom g = dom (- g) by NFCONT_4:def_3; f - g = f + (- g) by Lm1; hence integral ((f - g),c,d) = (integral (f,c,d)) + (integral ((- g),c,d)) by A1, A2, A3, Th27 .= (integral (f,c,d)) - (integral (g,c,d)) by A1, Th26 ; ::_thesis: verum end; theorem Th29: :: INTEGR19:29 for n being Element of NAT for a, b being real number 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 number 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 ) proof let n be Element of NAT ; ::_thesis: for a, b being real number 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 number 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 number ; ::_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 number 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 number 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 number 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 number 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 number st x in ['a,b'] holds ((proj (i,n)) * f) . x = (proj (i,n)) . E proof let x be real number ; ::_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, INTEGR15:def_15, INTEGR15:def_16; ::_thesis: verum end; theorem Th30: :: INTEGR19:30 for n being Element of NAT for a, b, c, d being real number for f being PartFunc of REAL,(REAL n) for E being Element of REAL n st a <= b & ( for x being real number st x in ['a,b'] holds f . x = E ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = (d - c) * E proof let n be Element of NAT ; ::_thesis: for a, b, c, d being real number for f being PartFunc of REAL,(REAL n) for E being Element of REAL n st a <= b & ( for x being real number st x in ['a,b'] holds f . x = E ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = (d - c) * E let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) for E being Element of REAL n st a <= b & ( for x being real number st x in ['a,b'] holds f . x = E ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = (d - c) * E let f be PartFunc of REAL,(REAL n); ::_thesis: for E being Element of REAL n st a <= b & ( for x being real number st x in ['a,b'] holds f . x = E ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = (d - c) * E let E be Element of REAL n; ::_thesis: ( a <= b & ( for x being real number st x in ['a,b'] holds f . x = E ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,c,d) = (d - c) * E ) assume A1: ( a <= b & ( for x being real number st x in ['a,b'] holds f . x = E ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral (f,c,d) = (d - c) * E A2: Seg n = dom (integral (f,c,d)) by INTEGR15:def_18; A3: now__::_thesis:_for_i_being_Element_of_NAT_holds_integral_(((proj_(i,n))_*_f),c,d)_=_((proj_(i,n))_._E)_*_(d_-_c) let i be Element of NAT ; ::_thesis: integral (((proj (i,n)) * f),c,d) = ((proj (i,n)) . E) * (d - c) set P = proj (i,n); dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then rng f c= dom (proj (i,n)) ; then A4: ['a,b'] c= dom ((proj (i,n)) * f) by A1, RELAT_1:27; for x being real number st x in ['a,b'] holds ((proj (i,n)) * f) . x = (proj (i,n)) . E proof let x be real number ; ::_thesis: ( x in ['a,b'] implies ((proj (i,n)) * f) . x = (proj (i,n)) . E ) assume A5: x in ['a,b'] ; ::_thesis: ((proj (i,n)) * f) . x = (proj (i,n)) . E then A6: f . x = f /. x by A1, PARTFUN1:def_6; ((proj (i,n)) * f) . x = (proj (i,n)) . (f /. x) by A4, A5, A6, FUNCT_1:12 .= (proj (i,n)) . E by A6, A5, A1 ; hence ((proj (i,n)) * f) . x = (proj (i,n)) . E ; ::_thesis: verum end; hence integral (((proj (i,n)) * f),c,d) = ((proj (i,n)) . E) * (d - c) by A4, A1, INTEGRA6:27; ::_thesis: verum end; A7: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(integral_(f,c,d))_holds_ (integral_(f,c,d))_._i_=_((d_-_c)_*_E)_._i let i be Nat; ::_thesis: ( i in dom (integral (f,c,d)) implies (integral (f,c,d)) . i = ((d - c) * E) . i ) set P = proj (i,n); assume A8: i in dom (integral (f,c,d)) ; ::_thesis: (integral (f,c,d)) . i = ((d - c) * E) . i hence (integral (f,c,d)) . i = integral (((proj (i,n)) * f),c,d) by A2, INTEGR15:def_18 .= ((proj (i,n)) . E) * (d - c) by A3, A8 .= (d - c) * (E . i) by PDIFF_1:def_1 .= ((d - c) * E) . i by RVSUM_1:44 ; ::_thesis: verum end; len ((d - c) * E) = n by CARD_1:def_7; then Seg n = dom ((d - c) * E) by FINSEQ_1:def_3; hence integral (f,c,d) = (d - c) * E by A2, A7, FINSEQ_1:13; ::_thesis: verum end; theorem Th31: :: INTEGR19:31 for n being Element of NAT for a, b, c, d being real number for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) proof let n be Element of NAT ; ::_thesis: for a, b, c, d being real number for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) ) assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ integral_(((proj_(i,n))_*_f),a,d)_=_(integral_(((proj_(i,n))_*_f),a,c))_+_(integral_(((proj_(i,n))_*_f),c,d)) let i be Element of NAT ; ::_thesis: ( i in Seg n implies integral (((proj (i,n)) * f),a,d) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,d)) ) set P = proj (i,n); assume A3: i in Seg n ; ::_thesis: integral (((proj (i,n)) * f),a,d) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,d)) then A4: (proj (i,n)) * f is_integrable_on ['a,b'] by A1, INTEGR15:def_16; (proj (i,n)) * (f | ['a,b']) is bounded by A3, A1, INTEGR15:def_15; 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; hence integral (((proj (i,n)) * f),a,d) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,d)) by A4, A5, A1, INTEGRA6:20; ::_thesis: verum end; A6: Seg n = dom (integral (f,a,d)) by INTEGR15:def_18; A7: now__::_thesis:_for_i0_being_Nat_st_i0_in_dom_(integral_(f,a,d))_holds_ (integral_(f,a,d))_._i0_=_((integral_(f,a,c))_+_(integral_(f,c,d)))_._i0 let i0 be Nat; ::_thesis: ( i0 in dom (integral (f,a,d)) implies (integral (f,a,d)) . i0 = ((integral (f,a,c)) + (integral (f,c,d))) . i0 ) assume A8: i0 in dom (integral (f,a,d)) ; ::_thesis: (integral (f,a,d)) . i0 = ((integral (f,a,c)) + (integral (f,c,d))) . i0 set P = proj (i0,n); thus (integral (f,a,d)) . i0 = integral (((proj (i0,n)) * f),a,d) by A8, A6, INTEGR15:def_18 .= (integral (((proj (i0,n)) * f),a,c)) + (integral (((proj (i0,n)) * f),c,d)) by A8, A2, A6 .= ((integral (f,a,c)) . i0) + (integral (((proj (i0,n)) * f),c,d)) by A8, A6, INTEGR15:def_18 .= ((integral (f,a,c)) . i0) + ((integral (f,c,d)) . i0) by A8, A6, INTEGR15:def_18 .= ((integral (f,a,c)) + (integral (f,c,d))) . i0 by RVSUM_1:11 ; ::_thesis: verum end; len ((integral (f,a,c)) + (integral (f,c,d))) = n by CARD_1:def_7; then Seg n = dom ((integral (f,a,c)) + (integral (f,c,d))) by FINSEQ_1:def_3; hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A6, A7, FINSEQ_1:13; ::_thesis: verum end; theorem Th32: :: INTEGR19:32 for n being Element of NAT for a, b, c, d, e being real number for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds |.(f /. x).| <= e ) holds |.(integral (f,c,d)).| <= (n * e) * (abs (d - c)) proof let n be Element of NAT ; ::_thesis: for a, b, c, d, e being real number for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds |.(f /. x).| <= e ) holds |.(integral (f,c,d)).| <= (n * e) * (abs (d - c)) let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds |.(f /. x).| <= e ) holds |.(integral (f,c,d)).| <= (n * e) * (abs (d - c)) let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds |.(f /. x).| <= e ) implies |.(integral (f,c,d)).| <= (n * e) * (abs (d - c)) ) assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds |.(f /. x).| <= e ) ) ; ::_thesis: |.(integral (f,c,d)).| <= (n * e) * (abs (d - c)) A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ |.(integral_(((proj_(i,n))_*_f),c,d)).|_<=_e_*_(abs_(d_-_c)) let i be Element of NAT ; ::_thesis: ( i in Seg n implies |.(integral (((proj (i,n)) * f),c,d)).| <= e * (abs (d - c)) ) set P = proj (i,n); assume A3: i in Seg n ; ::_thesis: |.(integral (((proj (i,n)) * f),c,d)).| <= e * (abs (d - c)) dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then rng f c= dom (proj (i,n)) ; then A4: ['a,b'] c= dom ((proj (i,n)) * f) by A1, RELAT_1:27; set f1 = (proj (i,n)) * f; A5: for x being real number st x in ['(min (c,d)),(max (c,d))'] holds |.(((proj (i,n)) * f) . x).| <= e proof let x be real number ; ::_thesis: ( x in ['(min (c,d)),(max (c,d))'] implies |.(((proj (i,n)) * f) . x).| <= e ) assume A6: x in ['(min (c,d)),(max (c,d))'] ; ::_thesis: |.(((proj (i,n)) * f) . x).| <= e ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A1, Lm2; then A7: x in dom ((proj (i,n)) * f) by A4, A6, TARSKI:def_3; then A8: x in dom f by FUNCT_1:11; A9: |.(f /. x).| <= e by A1, A6; A10: ((proj (i,n)) * f) . x = (proj (i,n)) . (f . x) by A7, FUNCT_1:12 .= (proj (i,n)) . (f /. x) by A8, PARTFUN1:def_6 ; ( 1 <= i & i <= n ) by A3, FINSEQ_1:1; then |.((proj (i,n)) . (f /. x)).| <= |.(f /. x).| by PDIFF_8:5; hence |.(((proj (i,n)) * f) . x).| <= e by A10, A9, XXREAL_0:2; ::_thesis: verum end; A11: (proj (i,n)) * f is_integrable_on ['a,b'] by A1, A3, INTEGR15:def_16; A12: (proj (i,n)) * (f | ['a,b']) is bounded by A1, A3, INTEGR15:def_15; ((proj (i,n)) * f) | ['a,b'] = (proj (i,n)) * (f | ['a,b']) by RELAT_1:83; hence |.(integral (((proj (i,n)) * f),c,d)).| <= e * (abs (d - c)) by A12, A1, A4, A5, A11, Lm4; ::_thesis: verum end; now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_n_holds_ |.((integral_(f,c,d))_._i).|_<=_e_*_(abs_(d_-_c)) let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies |.((integral (f,c,d)) . i).| <= e * (abs (d - c)) ) set P = proj (i,n); assume ( 1 <= i & i <= n ) ; ::_thesis: |.((integral (f,c,d)) . i).| <= e * (abs (d - c)) then A13: i in Seg n ; then |.(integral (((proj (i,n)) * f),c,d)).| <= e * (abs (d - c)) by A2; hence |.((integral (f,c,d)) . i).| <= e * (abs (d - c)) by A13, INTEGR15:def_18; ::_thesis: verum end; then |.(integral (f,c,d)).| <= n * (e * (abs (d - c))) by PDIFF_8:15; hence |.(integral (f,c,d)).| <= (n * e) * (abs (d - c)) ; ::_thesis: verum end; theorem Th33: :: INTEGR19:33 for n being Element of NAT for b, a being real number for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b)) proof let n be Element of NAT ; ::_thesis: for b, a being real number for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b)) let b, a be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b)) let f be PartFunc of REAL,(REAL n); ::_thesis: integral (f,b,a) = - (integral (f,a,b)) A1: ( a is Real & b is Real ) by XREAL_0:def_1; percases ( a <= b or not a <= b ) ; suppose a <= b ; ::_thesis: integral (f,b,a) = - (integral (f,a,b)) then A2: ['a,b'] = [.a,b.] by INTEGRA5:def_3; integral (f,['a,b']) = integral (f,a,b) by A1, A2, INTEGR15:19; hence integral (f,b,a) = - (integral (f,a,b)) by A1, A2, INTEGR15:20; ::_thesis: verum end; suppose not a <= b ; ::_thesis: integral (f,b,a) = - (integral (f,a,b)) then A3: ['b,a'] = [.b,a.] by INTEGRA5:def_3; then - (integral (f,['b,a'])) = integral (f,a,b) by A1, INTEGR15:20; hence integral (f,b,a) = - (integral (f,a,b)) by A1, A3, INTEGR15:19; ::_thesis: verum end; end; end; begin Lm16: for n being Element of NAT for p being FinSequence of REAL n for r being Element of REAL n for q being FinSequence of (REAL-NS n) st p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds r = Sum q proof let n be Element of NAT ; ::_thesis: for p being FinSequence of REAL n for r being Element of REAL n for q being FinSequence of (REAL-NS n) st p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds r = Sum q defpred S1[ Element of NAT ] means for p being FinSequence of REAL n for r being Element of REAL n for q being FinSequence of (REAL-NS n) st len p = $1 & p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds r = Sum q; A1: S1[ 0 ] proof let p be FinSequence of REAL n; ::_thesis: for r being Element of REAL n for q being FinSequence of (REAL-NS n) st len p = 0 & p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds r = Sum q let r be Element of REAL n; ::_thesis: for q being FinSequence of (REAL-NS n) st len p = 0 & p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds r = Sum q let q be FinSequence of (REAL-NS n); ::_thesis: ( len p = 0 & p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) implies r = Sum q ) assume A2: ( len p = 0 & p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) ) ; ::_thesis: r = Sum q then A3: p = {} ; A4: q = <*> the carrier of (REAL-NS n) by A2; len r = n by CARD_1:def_7; then A5: dom r = Seg n by FINSEQ_1:def_3; A6: dom ((Seg n) --> 0) = Seg n by FUNCOP_1:13; now__::_thesis:_for_x_being_set_st_x_in_dom_r_holds_ r_._x_=_((Seg_n)_-->_0)_._x let x be set ; ::_thesis: ( x in dom r implies r . x = ((Seg n) --> 0) . x ) assume A7: x in dom r ; ::_thesis: r . x = ((Seg n) --> 0) . x then reconsider i = x as Element of NAT ; set P = proj (i,n); consider Pi being FinSequence of REAL such that A8: ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) by A2, A5, A7; r . x = 0 by A3, A8, RVSUM_1:72; hence r . x = ((Seg n) --> 0) . x by A5, A7, FUNCOP_1:7; ::_thesis: verum end; then r = 0* n by A5, A6, FUNCT_1:2; then r = 0. (REAL-NS n) by REAL_NS1:def_4; hence r = Sum q by A4, RLVECT_1:43; ::_thesis: verum end; A9: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A10: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_p_being_FinSequence_of_REAL_n for_r_being_Element_of_REAL_n for_q_being_FinSequence_of_(REAL-NS_n)_st_len_p_=_k_+_1_&_p_=_q_&_(_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ ex_Pi_being_FinSequence_of_REAL_st_ (_Pi_=_(proj_(i,n))_*_p_&_r_._i_=_Sum_Pi_)_)_holds_ r_=_Sum_q let p be FinSequence of REAL n; ::_thesis: for r being Element of REAL n for q being FinSequence of (REAL-NS n) st len p = k + 1 & p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds r = Sum q let r be Element of REAL n; ::_thesis: for q being FinSequence of (REAL-NS n) st len p = k + 1 & p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds r = Sum q let q be FinSequence of (REAL-NS n); ::_thesis: ( len p = k + 1 & p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) implies r = Sum q ) assume A11: ( len p = k + 1 & p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) ) ; ::_thesis: r = Sum q set p1 = p | k; A12: k + 1 in Seg (k + 1) by FINSEQ_1:4; then k + 1 in dom p by A11, FINSEQ_1:def_3; then p . (k + 1) in rng p by FUNCT_1:3; then reconsider pk1 = p . (k + 1) as Element of REAL n ; set q1 = q | k; k + 1 in dom q by A11, A12, FINSEQ_1:def_3; then q . (k + 1) in rng q by FUNCT_1:3; then reconsider qk1 = q . (k + 1) as Point of (REAL-NS n) ; defpred S2[ Nat, set ] means ex P1i being FinSequence of REAL st ( P1i = (proj ($1,n)) * (p | k) & $2 = Sum P1i ); A13: for i being Nat st i in Seg n holds ex r being Element of REAL st S2[i,r] proof let i be Nat; ::_thesis: ( i in Seg n implies ex r being Element of REAL st S2[i,r] ) assume i in Seg n ; ::_thesis: ex r being Element of REAL st S2[i,r] take Sum ((proj (i,n)) * (p | k)) ; ::_thesis: S2[i, Sum ((proj (i,n)) * (p | k))] thus S2[i, Sum ((proj (i,n)) * (p | k))] ; ::_thesis: verum end; consider r1 being FinSequence of REAL such that A14: ( dom r1 = Seg n & ( for i being Nat st i in Seg n holds S2[i,r1 . i] ) ) from FINSEQ_1:sch_5(A13); len r1 = n by A14, FINSEQ_1:def_3; then reconsider r1 = r1 as Element of REAL n by FINSEQ_2:92; A15: for i being Element of NAT st i in Seg n holds ex P1i being FinSequence of REAL st ( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by A14; A16: k <= len p by A11, NAT_1:16; then A17: len (p | k) = k by FINSEQ_1:59; A18: r1 = Sum (q | k) by A10, A11, A15, A17; A19: len r = n by CARD_1:def_7; A20: len (r1 + pk1) = n by CARD_1:def_7; now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_n_holds_ r_._i_=_(r1_+_pk1)_._i let i be Nat; ::_thesis: ( 1 <= i & i <= n implies r . i = (r1 + pk1) . i ) set P = proj (i,n); assume ( 1 <= i & i <= n ) ; ::_thesis: r . i = (r1 + pk1) . i then A21: i in Seg n by FINSEQ_1:1; consider Pi being FinSequence of REAL such that A22: ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) by A21, A11; consider P1i being FinSequence of REAL such that A23: ( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by A21, A14; A24: dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then A25: rng p c= dom (proj (i,n)) ; A26: dom Pi = dom p by A25, A22, RELAT_1:27 .= Seg (len p) by FINSEQ_1:def_3 ; A27: len p = (len (p | k)) + 1 by A11, A16, FINSEQ_1:59 .= (len (p | k)) + (len <*(pk1 . i)*>) by FINSEQ_1:40 ; A28: rng (p | k) c= dom (proj (i,n)) by A24; A29: dom P1i = dom (p | k) by A28, A23, RELAT_1:27 .= Seg (len (p | k)) by FINSEQ_1:def_3 ; then A30: dom Pi = Seg ((len P1i) + (len <*(pk1 . i)*>)) by A26, A27, FINSEQ_1:def_3; len (p | k) <= len p by A16, FINSEQ_1:59; then A31: Seg (len (p | k)) c= Seg (len p) by FINSEQ_1:5; A32: for k being Nat st k in dom P1i holds Pi . k = P1i . k proof let k be Nat; ::_thesis: ( k in dom P1i implies Pi . k = P1i . k ) assume A33: k in dom P1i ; ::_thesis: Pi . k = P1i . k then A34: k in dom (p | k) by A29, FINSEQ_1:def_3; thus P1i . k = (proj (i,n)) . ((p | k) . k) by A23, A33, FUNCT_1:12 .= (proj (i,n)) . (p . k) by A34, FUNCT_1:47 .= Pi . k by A22, A33, A29, A26, A31, FUNCT_1:12 ; ::_thesis: verum end; for k being Nat st k in dom <*(pk1 . i)*> holds Pi . ((len P1i) + k) = <*(pk1 . i)*> . k proof let j be Nat; ::_thesis: ( j in dom <*(pk1 . i)*> implies Pi . ((len P1i) + j) = <*(pk1 . i)*> . j ) assume j in dom <*(pk1 . i)*> ; ::_thesis: Pi . ((len P1i) + j) = <*(pk1 . i)*> . j then j in Seg (len <*(pk1 . i)*>) by FINSEQ_1:def_3; then j in {1} by FINSEQ_1:2, FINSEQ_1:40; then A35: j = 1 by TARSKI:def_1; thus Pi . ((len P1i) + j) = Pi . (k + 1) by A29, A17, A35, FINSEQ_1:def_3 .= (proj (i,n)) . (p . (k + 1)) by A22, A26, A11, FINSEQ_1:4, FUNCT_1:12 .= pk1 . i by PDIFF_1:def_1 .= <*(pk1 . i)*> . j by A35, FINSEQ_1:40 ; ::_thesis: verum end; then Pi = P1i ^ <*(pk1 . i)*> by A32, A30, FINSEQ_1:def_7; hence r . i = (r1 . i) + (pk1 . i) by A22, A23, RVSUM_1:74 .= (r1 + pk1) . i by RVSUM_1:11 ; ::_thesis: verum end; then A36: r = r1 + pk1 by A19, A20, FINSEQ_1:14; A37: len q = (len (q | k)) + 1 by A16, A11, FINSEQ_1:59; A38: q | k = q | (dom (q | k)) by A17, A11, FINSEQ_1:def_3; thus r = (Sum (q | k)) + qk1 by A36, A18, A11, REAL_NS1:2 .= Sum q by A11, A37, A38, RLVECT_1:38 ; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A39: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A9); let p be FinSequence of REAL n; ::_thesis: for r being Element of REAL n for q being FinSequence of (REAL-NS n) st p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds r = Sum q let r be Element of REAL n; ::_thesis: for q being FinSequence of (REAL-NS n) st p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds r = Sum q let q be FinSequence of (REAL-NS n); ::_thesis: ( p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) implies r = Sum q ) assume A40: ( p = q & ( for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) ) ; ::_thesis: r = Sum q len p = len p ; hence r = Sum q by A40, A39; ::_thesis: verum end; definition let R be RealNormSpace; let X be non empty set ; let g be PartFunc of X,R; attrg is bounded means :Def1: :: INTEGR19:def 1 ex r being real number st for y being set st y in dom g holds ||.(g /. y).|| < r; end; :: deftheorem Def1 defines bounded INTEGR19:def_1_:_ for R being RealNormSpace for X being non empty set for g being PartFunc of X,R holds ( g is bounded iff ex r being real number st for y being set st y in dom g holds ||.(g /. y).|| < r ); theorem Th34: :: INTEGR19:34 for n being Element of NAT for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) st f = g holds ( f is bounded iff g is bounded ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) st f = g holds ( f is bounded iff g is bounded ) let f be PartFunc of REAL,(REAL n); ::_thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g holds ( f is bounded iff g is bounded ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f = g implies ( f is bounded iff g is bounded ) ) assume A1: f = g ; ::_thesis: ( f is bounded iff g is bounded ) thus ( f is bounded implies g is bounded ) ::_thesis: ( g is bounded implies f is bounded ) proof assume A2: f is bounded ; ::_thesis: g is bounded defpred S1[ Element of NAT , Element of REAL ] means for y being set st y in dom ((proj ($1,n)) * f) holds abs (((proj ($1,n)) * f) . y) < $2; A3: for i being Element of NAT st i in Seg n holds ex di being Element of REAL st S1[i,di] proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies ex di being Element of REAL st S1[i,di] ) set P = proj (i,n); assume i in Seg n ; ::_thesis: ex di being Element of REAL st S1[i,di] then (proj (i,n)) * f is bounded by A2, INTEGR15:def_15; then consider r being real number such that A4: for y being set st y in dom ((proj (i,n)) * f) holds abs (((proj (i,n)) * f) . y) < r by COMSEQ_2:def_3; reconsider r = r as Element of REAL by XREAL_0:def_1; take r ; ::_thesis: S1[i,r] thus S1[i,r] by A4; ::_thesis: verum end; consider d being FinSequence of REAL such that A5: ( dom d = Seg n & ( for k being Element of NAT st k in Seg n holds S1[k,d /. k] ) ) from RECDEF_1:sch_17(A3); set K = max d; for y being set st y in dom g holds ||.(g /. y).|| < (n * (max d)) + 1 proof let y be set ; ::_thesis: ( y in dom g implies ||.(g /. y).|| < (n * (max d)) + 1 ) assume A6: y in dom g ; ::_thesis: ||.(g /. y).|| < (n * (max d)) + 1 set s = f /. y; now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_n_holds_ abs_((f_/._y)_._i)_<=_max_d let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies abs ((f /. y) . i) <= max d ) set P = proj (i,n); assume A7: ( 1 <= i & i <= n ) ; ::_thesis: abs ((f /. y) . i) <= max d then A8: i in Seg n ; dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then rng f c= dom (proj (i,n)) ; then A9: y in dom ((proj (i,n)) * f) by A6, A1, RELAT_1:27; then A10: abs (((proj (i,n)) * f) . y) < d /. i by A8, A5; f . y = f /. y by A6, A1, PARTFUN1:def_6; then ((proj (i,n)) * f) . y = (proj (i,n)) . (f /. y) by A9, FUNCT_1:12; then A11: abs ((f /. y) . i) < d /. i by A10, PDIFF_1:def_1; len d = n by A5, FINSEQ_1:def_3; then d . i <= max d by A7, RFINSEQ2:1; then d /. i <= max d by A8, A5, PARTFUN1:def_6; hence abs ((f /. y) . i) <= max d by A11, XXREAL_0:2; ::_thesis: verum end; then A12: |.(f /. y).| < (n * (max d)) + 1 by PDIFF_8:15, XREAL_1:145; g /. y = g . y by A6, PARTFUN1:def_6 .= f /. y by A1, A6, PARTFUN1:def_6 ; hence ||.(g /. y).|| < (n * (max d)) + 1 by A12, REAL_NS1:1; ::_thesis: verum end; hence g is bounded by Def1; ::_thesis: verum end; assume A13: g is bounded ; ::_thesis: f is bounded consider r being real number such that A14: for y being set st y in dom g holds ||.(g /. y).|| < r by A13, Def1; let i be Element of NAT ; :: according to INTEGR15:def_15 ::_thesis: ( not i in Seg n or (proj (i,n)) * f is bounded ) set P = proj (i,n); assume A15: i in Seg n ; ::_thesis: (proj (i,n)) * f is bounded for y being set st y in dom ((proj (i,n)) * f) holds abs (((proj (i,n)) * f) . y) < r proof let y be set ; ::_thesis: ( y in dom ((proj (i,n)) * f) implies abs (((proj (i,n)) * f) . y) < r ) assume A16: y in dom ((proj (i,n)) * f) ; ::_thesis: abs (((proj (i,n)) * f) . y) < r dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then rng f c= dom (proj (i,n)) ; then A17: y in dom f by A16, RELAT_1:27; then A18: ||.(g /. y).|| < r by A14, A1; set s = f /. y; g /. y = g . y by A17, A1, PARTFUN1:def_6 .= f /. y by A1, A17, PARTFUN1:def_6 ; then A19: |.(f /. y).| < r by A18, REAL_NS1:1; abs ((f /. y) . i) <= |.(f /. y).| by A15, REAL_NS1:8; then A20: abs ((f /. y) . i) < r by A19, XXREAL_0:2; f . y = f /. y by A17, PARTFUN1:def_6; then ((proj (i,n)) * f) . y = (proj (i,n)) . (f /. y) by A16, FUNCT_1:12; hence abs (((proj (i,n)) * f) . y) < r by A20, PDIFF_1:def_1; ::_thesis: verum end; hence (proj (i,n)) * f is bounded by COMSEQ_2:def_3; ::_thesis: verum end; theorem Th35: :: INTEGR19:35 for n being Element of NAT for X, Y being set for f1, f2 being PartFunc of REAL,(REAL-NS n) st f1 | X is bounded & f2 | Y is bounded holds ( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) proof let n be Element of NAT ; ::_thesis: for X, Y being set for f1, f2 being PartFunc of REAL,(REAL-NS n) st f1 | X is bounded & f2 | Y is bounded holds ( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) let X, Y be set ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL-NS n) st f1 | X is bounded & f2 | Y is bounded holds ( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) let f1, f2 be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f1 | X is bounded & f2 | Y is bounded implies ( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) ) assume A1: ( f1 | X is bounded & f2 | Y is bounded ) ; ::_thesis: ( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) consider r1 being real number such that A2: for x being set st x in dom (f1 | X) holds ||.((f1 | X) /. x).|| < r1 by A1, Def1; consider r2 being real number such that A3: for x being set st x in dom (f2 | Y) holds ||.((f2 | Y) /. x).|| < r2 by A1, Def1; now__::_thesis:_for_x_being_set_st_x_in_dom_((f1_+_f2)_|_(X_/\_Y))_holds_ ||.(((f1_+_f2)_|_(X_/\_Y))_/._x).||_<_r1_+_r2 let x be set ; ::_thesis: ( x in dom ((f1 + f2) | (X /\ Y)) implies ||.(((f1 + f2) | (X /\ Y)) /. x).|| < r1 + r2 ) assume x in dom ((f1 + f2) | (X /\ Y)) ; ::_thesis: ||.(((f1 + f2) | (X /\ Y)) /. x).|| < r1 + r2 then A4: ( x in dom (f1 + f2) & x in X /\ Y ) by RELAT_1:57; then x in (dom f1) /\ (dom f2) by VFUNCT_1:def_1; then A5: ( x in dom f1 & x in dom f2 ) by XBOOLE_0:def_4; A6: ( x in X & x in Y ) by A4, XBOOLE_0:def_4; ((f1 + f2) | (X /\ Y)) /. x = (f1 + f2) /. x by A4, PARTFUN2:17 .= (f1 /. x) + (f2 /. x) by A4, VFUNCT_1:def_1 .= ((f1 | X) /. x) + (f2 /. x) by A5, A6, PARTFUN2:17 .= ((f1 | X) /. x) + ((f2 | Y) /. x) by A5, A6, PARTFUN2:17 ; then A7: ||.(((f1 + f2) | (X /\ Y)) /. x).|| <= ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| by NORMSP_1:def_1; x in dom (f1 | X) by A5, A6, RELAT_1:57; then A8: ||.((f1 | X) /. x).|| < r1 by A2; x in dom (f2 | Y) by A5, A6, RELAT_1:57; then ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| < r1 + r2 by A3, A8, XREAL_1:8; hence ||.(((f1 + f2) | (X /\ Y)) /. x).|| < r1 + r2 by A7, XXREAL_0:2; ::_thesis: verum end; hence (f1 + f2) | (X /\ Y) is bounded by Def1; ::_thesis: (f1 - f2) | (X /\ Y) is bounded take r1 + r2 ; :: according to INTEGR19:def_1 ::_thesis: for y being set st y in dom ((f1 - f2) | (X /\ Y)) holds ||.(((f1 - f2) | (X /\ Y)) /. y).|| < r1 + r2 let x be set ; ::_thesis: ( x in dom ((f1 - f2) | (X /\ Y)) implies ||.(((f1 - f2) | (X /\ Y)) /. x).|| < r1 + r2 ) assume x in dom ((f1 - f2) | (X /\ Y)) ; ::_thesis: ||.(((f1 - f2) | (X /\ Y)) /. x).|| < r1 + r2 then A9: ( x in dom (f1 - f2) & x in X /\ Y ) by RELAT_1:57; then x in (dom f1) /\ (dom f2) by VFUNCT_1:def_2; then A10: ( x in dom f1 & x in dom f2 ) by XBOOLE_0:def_4; A11: ( x in X & x in Y ) by A9, XBOOLE_0:def_4; ((f1 - f2) | (X /\ Y)) /. x = (f1 - f2) /. x by A9, PARTFUN2:17 .= (f1 /. x) - (f2 /. x) by A9, VFUNCT_1:def_2 .= ((f1 | X) /. x) - (f2 /. x) by A10, A11, PARTFUN2:17 .= ((f1 | X) /. x) - ((f2 | Y) /. x) by A10, A11, PARTFUN2:17 ; then A12: ||.(((f1 - f2) | (X /\ Y)) /. x).|| <= ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| by NORMSP_1:3; x in dom (f1 | X) by A10, A11, RELAT_1:57; then A13: ||.((f1 | X) /. x).|| < r1 by A2; x in dom (f2 | Y) by A10, A11, RELAT_1:57; then ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| < r1 + r2 by A13, A3, XREAL_1:8; hence ||.(((f1 - f2) | (X /\ Y)) /. x).|| < r1 + r2 by A12, XXREAL_0:2; ::_thesis: verum end; theorem Th36: :: INTEGR19:36 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for D being Division of A for p being FinSequence of REAL n for q being FinSequence of (REAL-NS n) st f = g & p = q holds ( p is middle_volume of f,D iff q is middle_volume of g,D ) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for D being Division of A for p being FinSequence of REAL n for q being FinSequence of (REAL-NS n) st f = g & p = q holds ( p is middle_volume of f,D iff q is middle_volume of g,D ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for D being Division of A for p being FinSequence of REAL n for q being FinSequence of (REAL-NS n) st f = g & p = q holds ( p is middle_volume of f,D iff q is middle_volume of g,D ) let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n) for D being Division of A for p being FinSequence of REAL n for q being FinSequence of (REAL-NS n) st f = g & p = q holds ( p is middle_volume of f,D iff q is middle_volume of g,D ) let g be Function of A,(REAL-NS n); ::_thesis: for D being Division of A for p being FinSequence of REAL n for q being FinSequence of (REAL-NS n) st f = g & p = q holds ( p is middle_volume of f,D iff q is middle_volume of g,D ) let D be Division of A; ::_thesis: for p being FinSequence of REAL n for q being FinSequence of (REAL-NS n) st f = g & p = q holds ( p is middle_volume of f,D iff q is middle_volume of g,D ) let p be FinSequence of REAL n; ::_thesis: for q being FinSequence of (REAL-NS n) st f = g & p = q holds ( p is middle_volume of f,D iff q is middle_volume of g,D ) let q be FinSequence of (REAL-NS n); ::_thesis: ( f = g & p = q implies ( p is middle_volume of f,D iff q is middle_volume of g,D ) ) assume A1: ( f = g & p = q ) ; ::_thesis: ( p is middle_volume of f,D iff q is middle_volume of g,D ) thus ( p is middle_volume of f,D implies q is middle_volume of g,D ) ::_thesis: ( q is middle_volume of g,D implies p is middle_volume of f,D ) proof assume A2: p is middle_volume of f,D ; ::_thesis: q is middle_volume of g,D then A3: len q = len D by A1, INTEGR15:def_5; for i being Nat st i in dom D holds ex c being Point of (REAL-NS n) st ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) proof let i be Nat; ::_thesis: ( i in dom D implies ex c being Point of (REAL-NS n) st ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) ) assume i in dom D ; ::_thesis: ex c being Point of (REAL-NS n) st ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) then consider r being Element of REAL n such that A4: ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) by A2, INTEGR15:def_5; reconsider c = r as Point of (REAL-NS n) by REAL_NS1:def_4; take c ; ::_thesis: ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) thus ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) by A4, A1, REAL_NS1:3; ::_thesis: verum end; hence q is middle_volume of g,D by A3, INTEGR18:def_1; ::_thesis: verum end; thus ( q is middle_volume of g,D implies p is middle_volume of f,D ) ::_thesis: verum proof assume A5: q is middle_volume of g,D ; ::_thesis: p is middle_volume of f,D then A6: len p = len D by A1, INTEGR18:def_1; for i being Nat st i in dom D holds ex r being Element of REAL n st ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) proof let i be Nat; ::_thesis: ( i in dom D implies ex r being Element of REAL n st ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) ) assume A7: i in dom D ; ::_thesis: ex r being Element of REAL n st ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) consider c being Point of (REAL-NS n) such that A8: ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) by A5, A7, INTEGR18:def_1; reconsider r = c as Element of REAL n by REAL_NS1:def_4; take r ; ::_thesis: ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) thus ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) by A8, A1, REAL_NS1:3; ::_thesis: verum end; hence p is middle_volume of f,D by A6, INTEGR15:def_5; ::_thesis: verum end; end; theorem Th37: :: INTEGR19:37 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for D being Division of A for p being middle_volume of f,D for q being middle_volume of g,D st f = g & p = q holds middle_sum (f,p) = middle_sum (g,q) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for D being Division of A for p being middle_volume of f,D for q being middle_volume of g,D st f = g & p = q holds middle_sum (f,p) = middle_sum (g,q) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for D being Division of A for p being middle_volume of f,D for q being middle_volume of g,D st f = g & p = q holds middle_sum (f,p) = middle_sum (g,q) let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n) for D being Division of A for p being middle_volume of f,D for q being middle_volume of g,D st f = g & p = q holds middle_sum (f,p) = middle_sum (g,q) let g be Function of A,(REAL-NS n); ::_thesis: for D being Division of A for p being middle_volume of f,D for q being middle_volume of g,D st f = g & p = q holds middle_sum (f,p) = middle_sum (g,q) let D be Division of A; ::_thesis: for p being middle_volume of f,D for q being middle_volume of g,D st f = g & p = q holds middle_sum (f,p) = middle_sum (g,q) let p be middle_volume of f,D; ::_thesis: for q being middle_volume of g,D st f = g & p = q holds middle_sum (f,p) = middle_sum (g,q) let q be middle_volume of g,D; ::_thesis: ( f = g & p = q implies middle_sum (f,p) = middle_sum (g,q) ) assume A1: ( f = g & p = q ) ; ::_thesis: middle_sum (f,p) = middle_sum (g,q) for i being Element of NAT st i in Seg n holds ex Pi being FinSequence of REAL st ( Pi = (proj (i,n)) * p & (middle_sum (f,p)) . i = Sum Pi ) by INTEGR15:def_6; hence middle_sum (f,p) = middle_sum (g,q) by Lm16, A1; ::_thesis: verum end; theorem Th38: :: INTEGR19:38 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for T being DivSequence of A for p being Function of NAT,((REAL n) *) for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T ) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for T being DivSequence of A for p being Function of NAT,((REAL n) *) for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for T being DivSequence of A for p being Function of NAT,((REAL n) *) for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T ) let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n) for T being DivSequence of A for p being Function of NAT,((REAL n) *) for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T ) let g be Function of A,(REAL-NS n); ::_thesis: for T being DivSequence of A for p being Function of NAT,((REAL n) *) for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T ) let T be DivSequence of A; ::_thesis: for p being Function of NAT,((REAL n) *) for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T ) let p be Function of NAT,((REAL n) *); ::_thesis: for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T ) let q be Function of NAT,( the carrier of (REAL-NS n) *); ::_thesis: ( f = g & p = q implies ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T ) ) assume A1: ( f = g & p = q ) ; ::_thesis: ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T ) hereby ::_thesis: ( q is middle_volume_Sequence of g,T implies p is middle_volume_Sequence of f,T ) assume A2: p is middle_volume_Sequence of f,T ; ::_thesis: q is middle_volume_Sequence of g,T for k being Element of NAT holds q . k is middle_volume of g,T . k proof let k be Element of NAT ; ::_thesis: q . k is middle_volume of g,T . k A3: p . k is middle_volume of f,T . k by A2, INTEGR15:def_7; q . k is FinSequence of (REAL-NS n) by FINSEQ_2:def_3; hence q . k is middle_volume of g,T . k by A1, A3, Th36; ::_thesis: verum end; hence q is middle_volume_Sequence of g,T by INTEGR18:def_3; ::_thesis: verum end; assume A4: q is middle_volume_Sequence of g,T ; ::_thesis: p is middle_volume_Sequence of f,T for k being Element of NAT holds p . k is middle_volume of f,T . k proof let k be Element of NAT ; ::_thesis: p . k is middle_volume of f,T . k A5: q . k is middle_volume of g,T . k by A4, INTEGR18:def_3; p . k is FinSequence of REAL n by FINSEQ_2:def_3; hence p . k is middle_volume of f,T . k by A1, A5, Th36; ::_thesis: verum end; hence p is middle_volume_Sequence of f,T by INTEGR15:def_7; ::_thesis: verum end; theorem Th39: :: INTEGR19:39 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for T being DivSequence of A for S being middle_volume_Sequence of f,T for U being middle_volume_Sequence of g,T st f = g & S = U holds middle_sum (f,S) = middle_sum (g,U) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for T being DivSequence of A for S being middle_volume_Sequence of f,T for U being middle_volume_Sequence of g,T st f = g & S = U holds middle_sum (f,S) = middle_sum (g,U) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for T being DivSequence of A for S being middle_volume_Sequence of f,T for U being middle_volume_Sequence of g,T st f = g & S = U holds middle_sum (f,S) = middle_sum (g,U) let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n) for T being DivSequence of A for S being middle_volume_Sequence of f,T for U being middle_volume_Sequence of g,T st f = g & S = U holds middle_sum (f,S) = middle_sum (g,U) let g be Function of A,(REAL-NS n); ::_thesis: for T being DivSequence of A for S being middle_volume_Sequence of f,T for U being middle_volume_Sequence of g,T st f = g & S = U holds middle_sum (f,S) = middle_sum (g,U) let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of f,T for U being middle_volume_Sequence of g,T st f = g & S = U holds middle_sum (f,S) = middle_sum (g,U) let S be middle_volume_Sequence of f,T; ::_thesis: for U being middle_volume_Sequence of g,T st f = g & S = U holds middle_sum (f,S) = middle_sum (g,U) let U be middle_volume_Sequence of g,T; ::_thesis: ( f = g & S = U implies middle_sum (f,S) = middle_sum (g,U) ) assume A1: ( f = g & S = U ) ; ::_thesis: middle_sum (f,S) = middle_sum (g,U) A2: dom (middle_sum (f,S)) = NAT by FUNCT_2:def_1 .= dom (middle_sum (g,U)) by FUNCT_2:def_1 ; now__::_thesis:_for_x_being_set_st_x_in_dom_(middle_sum_(f,S))_holds_ (middle_sum_(f,S))_._x_=_(middle_sum_(g,U))_._x let x be set ; ::_thesis: ( x in dom (middle_sum (f,S)) implies (middle_sum (f,S)) . x = (middle_sum (g,U)) . x ) assume x in dom (middle_sum (f,S)) ; ::_thesis: (middle_sum (f,S)) . x = (middle_sum (g,U)) . x then reconsider n = x as Element of NAT ; A3: middle_sum (f,(S . n)) = middle_sum (g,(U . n)) by A1, Th37; thus (middle_sum (f,S)) . x = middle_sum (f,(S . n)) by INTEGR15:def_8 .= (middle_sum (g,U)) . x by A3, INTEGR18:def_4 ; ::_thesis: verum end; hence middle_sum (f,S) = middle_sum (g,U) by A2, FUNCT_1:2; ::_thesis: verum end; theorem Th40: :: INTEGR19:40 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for I being Element of REAL n for J being Point of (REAL-NS n) st f = g & I = J holds ( ( for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for I being Element of REAL n for J being Point of (REAL-NS n) st f = g & I = J holds ( ( for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) for I being Element of REAL n for J being Point of (REAL-NS n) st f = g & I = J holds ( ( for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n) for I being Element of REAL n for J being Point of (REAL-NS n) st f = g & I = J holds ( ( for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) let g be Function of A,(REAL-NS n); ::_thesis: for I being Element of REAL n for J being Point of (REAL-NS n) st f = g & I = J holds ( ( for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) let I be Element of REAL n; ::_thesis: for J being Point of (REAL-NS n) st f = g & I = J holds ( ( for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) let J be Point of (REAL-NS n); ::_thesis: ( f = g & I = J implies ( ( for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) ) assume A1: ( f = g & I = J ) ; ::_thesis: ( ( for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) hereby ::_thesis: ( ( for T being DivSequence of A for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) implies for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) assume A2: for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; ::_thesis: for T being DivSequence of A for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) A3: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4; thus for T being DivSequence of A for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) ::_thesis: verum proof let T be DivSequence of A; ::_thesis: for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) let S0 be middle_volume_Sequence of g,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) ) assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) reconsider S = S0 as middle_volume_Sequence of f,T by A3, A1, Th38; ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A2, A4; hence ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) by A1, Th39; ::_thesis: verum end; end; assume A5: for T being DivSequence of A for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ; ::_thesis: for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) A6: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4; thus for T being DivSequence of A for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) ::_thesis: verum proof let T be DivSequence of A; ::_thesis: for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) let S0 be middle_volume_Sequence of f,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) ) assume A7: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) reconsider S = S0 as middle_volume_Sequence of g,T by A6, A1, Th38; ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = I ) by A1, A5, A7; hence ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) by A1, Th39; ::_thesis: verum end; end; theorem Th41: :: INTEGR19:41 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) st f = g & f is bounded holds ( f is integrable iff g is integrable ) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) st f = g & f is bounded holds ( f is integrable iff g is integrable ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) st f = g & f is bounded holds ( f is integrable iff g is integrable ) let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n) st f = g & f is bounded holds ( f is integrable iff g is integrable ) let g be Function of A,(REAL-NS n); ::_thesis: ( f = g & f is bounded implies ( f is integrable iff g is integrable ) ) assume A1: ( f = g & f is bounded ) ; ::_thesis: ( f is integrable iff g is integrable ) hereby ::_thesis: ( g is integrable implies f is integrable ) assume f is integrable ; ::_thesis: g is integrable then consider I being Element of REAL n such that A2: for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A1, INTEGR15:12; reconsider I0 = I as Point of (REAL-NS n) by REAL_NS1:def_4; I = I0 ; then for T being DivSequence of A for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = I0 ) by A2, A1, Th40; hence g is integrable by INTEGR18:def_5; ::_thesis: verum end; assume g is integrable ; ::_thesis: f is integrable then consider I being Point of (REAL-NS n) such that A3: for T being DivSequence of A for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = I ) by INTEGR18:def_5; reconsider I0 = I as Element of REAL n by REAL_NS1:def_4; I0 = I ; then for T being DivSequence of A for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I0 ) by A3, A1, Th40; hence f is integrable by A1, INTEGR15:12; ::_thesis: verum end; theorem Th42: :: INTEGR19:42 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) st f = g & f is bounded & f is integrable holds ( g is integrable & integral f = integral g ) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) st f = g & f is bounded & f is integrable holds ( g is integrable & integral f = integral g ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n) for g being Function of A,(REAL-NS n) st f = g & f is bounded & f is integrable holds ( g is integrable & integral f = integral g ) let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n) st f = g & f is bounded & f is integrable holds ( g is integrable & integral f = integral g ) let g be Function of A,(REAL-NS n); ::_thesis: ( f = g & f is bounded & f is integrable implies ( g is integrable & integral f = integral g ) ) assume A1: ( f = g & f is bounded & f is integrable ) ; ::_thesis: ( g is integrable & integral f = integral g ) then A2: g is integrable by Th41; A3: for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) by A1, INTEGR15:11; reconsider I0 = integral f as Point of (REAL-NS n) by REAL_NS1:def_4; integral f = I0 ; then for T being DivSequence of A for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = I0 ) by A3, A1, Th40; hence ( g is integrable & integral f = integral g ) by A2, INTEGR18:def_6; ::_thesis: verum end; theorem Th43: :: INTEGR19:43 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f holds ( f is_integrable_on A iff g is_integrable_on A ) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f holds ( f is_integrable_on A iff g is_integrable_on A ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f holds ( f is_integrable_on A iff g is_integrable_on A ) let f be PartFunc of REAL,(REAL n); ::_thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f holds ( f is_integrable_on A iff g is_integrable_on A ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f = g & f | A is bounded & A c= dom f implies ( f is_integrable_on A iff g is_integrable_on A ) ) assume A1: ( f = g & f | A is bounded & A c= dom f ) ; ::_thesis: ( f is_integrable_on A iff g is_integrable_on A ) reconsider h = f | A as Function of A,(REAL n) by Lm3, A1; reconsider k = h as Function of A,(REAL-NS n) by REAL_NS1:def_4; A2: h is bounded by A1, Th16; hereby ::_thesis: ( g is_integrable_on A implies f is_integrable_on A ) assume f is_integrable_on A ; ::_thesis: g is_integrable_on A then h is integrable by INTEGR15:13; then k is integrable by A2, Th41; hence g is_integrable_on A by A1, INTEGR18:def_7; ::_thesis: verum end; assume g is_integrable_on A ; ::_thesis: f is_integrable_on A then k is integrable by A1, INTEGR18:8; then h is integrable by A2, Th41; hence f is_integrable_on A by INTEGR15:13; ::_thesis: verum end; theorem Th44: :: INTEGR19:44 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds ( g is_integrable_on A & integral (f,A) = integral (g,A) ) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds ( g is_integrable_on A & integral (f,A) = integral (g,A) ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds ( g is_integrable_on A & integral (f,A) = integral (g,A) ) let f be PartFunc of REAL,(REAL n); ::_thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds ( g is_integrable_on A & integral (f,A) = integral (g,A) ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f = g & f | A is bounded & A c= dom f & f is_integrable_on A implies ( g is_integrable_on A & integral (f,A) = integral (g,A) ) ) assume A1: ( f = g & f | A is bounded & A c= dom f & f is_integrable_on A ) ; ::_thesis: ( g is_integrable_on A & integral (f,A) = integral (g,A) ) hence g is_integrable_on A by Th43; ::_thesis: integral (f,A) = integral (g,A) reconsider h = f | A as Function of A,(REAL n) by Lm3, A1; reconsider k = h as Function of A,(REAL-NS n) by REAL_NS1:def_4; A2: integral (f,A) = integral h by INTEGR15:14; A3: h is bounded by A1, Th16; h is integrable by A1, INTEGR15:13; then integral h = integral k by A3, Th42; hence integral (f,A) = integral (g,A) by A2, A1, INTEGR18:9; ::_thesis: verum end; theorem Th45: :: INTEGR19:45 for n being Element of NAT for a, b being real number for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) st f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] holds integral (f,a,b) = integral (g,a,b) proof let n be Element of NAT ; ::_thesis: for a, b being real number for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) st f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] holds integral (f,a,b) = integral (g,a,b) let a, b be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) for g being PartFunc of REAL,(REAL-NS n) st f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] holds integral (f,a,b) = integral (g,a,b) let f be PartFunc of REAL,(REAL n); ::_thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] holds integral (f,a,b) = integral (g,a,b) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] implies integral (f,a,b) = integral (g,a,b) ) assume A1: ( f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] ) ; ::_thesis: integral (f,a,b) = integral (g,a,b) A2: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; A3: integral (g,['a,b']) = integral (f,['a,b']) by A1, Th44; A4: ( a is Real & b is Real ) by XREAL_0:def_1; then integral (g,['a,b']) = integral (g,a,b) by A2, INTEGR18:16; hence integral (f,a,b) = integral (g,a,b) by A3, A2, A4, INTEGR15:19; ::_thesis: verum end; theorem :: INTEGR19:46 for n being Element of NAT for a, b being real number for f, g being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g holds ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) proof let n be Element of NAT ; ::_thesis: for a, b being real number for f, g being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g holds ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) let a, b be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g holds ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) let f, g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g implies ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) ) assume A1: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g ) ; ::_thesis: ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) A2: ( f + g is_integrable_on ['a,b'] & integral ((f + g),['a,b']) = (integral (f,['a,b'])) + (integral (g,['a,b'])) ) by A1, INTEGR18:14; A3: ( f - g is_integrable_on ['a,b'] & integral ((f - g),['a,b']) = (integral (f,['a,b'])) - (integral (g,['a,b'])) ) by A1, INTEGR18:15; A4: ( a is Real & b is Real ) by XREAL_0:def_1; A5: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; thus integral ((f + g),a,b) = integral ((f + g),['a,b']) by A5, A4, INTEGR18:16 .= (integral (f,a,b)) + (integral (g,['a,b'])) by A5, A4, A2, INTEGR18:16 .= (integral (f,a,b)) + (integral (g,a,b)) by A5, A4, INTEGR18:16 ; ::_thesis: integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) thus integral ((f - g),a,b) = integral ((f - g),['a,b']) by A5, A4, INTEGR18:16 .= (integral (f,a,b)) - (integral (g,['a,b'])) by A5, A4, A3, INTEGR18:16 .= (integral (f,a,b)) - (integral (g,a,b)) by A5, A4, INTEGR18:16 ; ::_thesis: verum end; theorem Th47: :: INTEGR19:47 for n being Element of NAT for a, b being real number for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f holds integral (f,b,a) = - (integral (f,a,b)) proof let n be Element of NAT ; ::_thesis: for a, b being real number for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f holds integral (f,b,a) = - (integral (f,a,b)) let a, b be real number ; ::_thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f holds integral (f,b,a) = - (integral (f,a,b)) let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & ['a,b'] c= dom f implies integral (f,b,a) = - (integral (f,a,b)) ) assume A1: ( a <= b & ['a,b'] c= dom f ) ; ::_thesis: integral (f,b,a) = - (integral (f,a,b)) then A2: ['a,b'] = [.a,b.] by INTEGRA5:def_3; A3: ( a is Real & b is Real ) by XREAL_0:def_1; then integral (f,['a,b']) = integral (f,a,b) by A2, INTEGR18:16; hence integral (f,b,a) = - (integral (f,a,b)) by A3, A2, A1, INTEGR18:18; ::_thesis: verum end; theorem Th48: :: INTEGR19:48 for n being Element of NAT for a, b, c, d being real number for f being PartFunc of REAL,(REAL-NS n) for g being PartFunc of REAL,(REAL n) st f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = integral (g,c,d) proof let n be Element of NAT ; ::_thesis: for a, b, c, d being real number for f being PartFunc of REAL,(REAL-NS n) for g being PartFunc of REAL,(REAL n) st f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = integral (g,c,d) let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,(REAL-NS n) for g being PartFunc of REAL,(REAL n) st f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = integral (g,c,d) let f be PartFunc of REAL,(REAL-NS n); ::_thesis: for g being PartFunc of REAL,(REAL n) st f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = integral (g,c,d) let g be PartFunc of REAL,(REAL n); ::_thesis: ( f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] implies integral (f,c,d) = integral (g,c,d) ) assume A1: ( f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral (f,c,d) = integral (g,c,d) ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A2: ( a <= c & d <= b & a <= d & c <= b ) by A1, XXREAL_1:1; A3: g | ['a,b'] is bounded by A1, Th34; A4: g is_integrable_on ['a,b'] by Th43, A3, A1; percases ( c <= d or not c <= d ) ; supposeA5: c <= d ; ::_thesis: integral (f,c,d) = integral (g,c,d) ( ['c,d'] c= dom g & g | ['c,d'] is bounded & g is_integrable_on ['c,d'] ) by A3, A4, A1, Th9, A2, A5, Th2; hence integral (f,c,d) = integral (g,c,d) by A1, A5, Th45; ::_thesis: verum end; supposeA6: not c <= d ; ::_thesis: integral (f,c,d) = integral (g,c,d) A7: ( ['d,c'] c= dom g & g | ['d,c'] is bounded & g is_integrable_on ['d,c'] ) by A3, A4, A1, Th9, A2, A6, Th2; then A8: integral (f,d,c) = integral (g,d,c) by A1, A6, Th45; thus integral (g,c,d) = - (integral (g,d,c)) by Th33 .= - (integral (f,d,c)) by A8, REAL_NS1:4 .= integral (f,c,d) by A6, A7, A1, Th47 ; ::_thesis: verum end; end; end; theorem :: INTEGR19:49 for n being Element of NAT for a, b, c, d being real number for f, g being PartFunc of REAL,(REAL-NS n) st a <= 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 & c in ['a,b'] & d in ['a,b'] holds integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) proof let n be Element of NAT ; ::_thesis: for a, b, c, d being real number for f, g being PartFunc of REAL,(REAL-NS n) st a <= 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 & c in ['a,b'] & d in ['a,b'] holds integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) let a, b, c, d be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL-NS n) st a <= 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 & c in ['a,b'] & d in ['a,b'] holds integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) let f, g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= 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 & c in ['a,b'] & d in ['a,b'] implies integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) ) assume A1: ( a <= 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 & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) reconsider f1 = f, g1 = g as PartFunc of REAL,(REAL n) by REAL_NS1:def_4; A2: f1 | ['a,b'] is bounded by Th34, A1; A3: g1 | ['a,b'] is bounded by Th34, A1; A4: f1 is_integrable_on ['a,b'] by Th43, A2, A1; A5: g1 is_integrable_on ['a,b'] by Th43, A3, A1; A6: f1 + g1 = f + g by NFCONT_4:5; A7: ( integral (f1,c,d) = integral (f,c,d) & integral (g1,c,d) = integral (g,c,d) ) by A1, Th48; A8: ['a,b'] c= dom (f + g) by A1, A6, Th4; ( f1 + g1 is_integrable_on ['a,b'] & (f1 + g1) | ['a,b'] is bounded ) by A1, A2, A3, A4, A5, Th10; then ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) by Th43, A6, A8, Th34; hence integral ((f + g),c,d) = integral ((f1 + g1),c,d) by A1, A8, Th48, NFCONT_4:5 .= (integral (f1,c,d)) + (integral (g1,c,d)) by A1, A2, A3, A4, A5, Th27 .= (integral (f,c,d)) + (integral (g,c,d)) by A7, REAL_NS1:2 ; ::_thesis: verum end; theorem Th50: :: INTEGR19:50 for n being Element of NAT for a, b, c, d being real number for f, g being PartFunc of REAL,(REAL-NS n) st a <= 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 & c in ['a,b'] & d in ['a,b'] holds integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) proof let n be Element of NAT ; ::_thesis: for a, b, c, d being real number for f, g being PartFunc of REAL,(REAL-NS n) st a <= 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 & c in ['a,b'] & d in ['a,b'] holds integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) let a, b, c, d be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL-NS n) st a <= 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 & c in ['a,b'] & d in ['a,b'] holds integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) let f, g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= 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 & c in ['a,b'] & d in ['a,b'] implies integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) assume A1: ( a <= 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 & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) reconsider f1 = f, g1 = g as PartFunc of REAL,(REAL n) by REAL_NS1:def_4; A2: f1 | ['a,b'] is bounded by Th34, A1; A3: g1 | ['a,b'] is bounded by Th34, A1; A4: f1 is_integrable_on ['a,b'] by Th43, A2, A1; A5: g1 is_integrable_on ['a,b'] by Th43, A3, A1; A6: f1 - g1 = f - g by NFCONT_4:10; A7: ( integral (f1,c,d) = integral (f,c,d) & integral (g1,c,d) = integral (g,c,d) ) by A1, Th48; A8: ['a,b'] c= dom (f - g) by A1, A6, Th5; ( f1 - g1 is_integrable_on ['a,b'] & (f1 - g1) | ['a,b'] is bounded ) by A1, A2, A3, A4, A5, Th13; then ( f - g is_integrable_on ['a,b'] & (f - g) | ['a,b'] is bounded ) by Th43, A6, A8, Th34; hence integral ((f - g),c,d) = integral ((f1 - g1),c,d) by A1, A8, Th48, NFCONT_4:10 .= (integral (f1,c,d)) - (integral (g1,c,d)) by A1, A2, A3, A4, A5, Th28 .= (integral (f,c,d)) - (integral (g,c,d)) by A7, REAL_NS1:5 ; ::_thesis: verum end; theorem Th51: :: INTEGR19:51 for n being Element of NAT for a, b being real number for E being Point of (REAL-NS n) for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number 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 ) proof let n be Element of NAT ; ::_thesis: for a, b being real number for E being Point of (REAL-NS n) for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number 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 number ; ::_thesis: for E being Point of (REAL-NS n) for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number 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 Point of (REAL-NS n); ::_thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number 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-NS n); ::_thesis: ( a <= b & ['a,b'] c= dom f & ( for x being real number 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 number 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 ) reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def_4; reconsider e1 = e as Element of REAL n by REAL_NS1:def_4; A2: for x being real number st x in ['a,b'] holds f1 . x = e1 by A1; A3: ( f1 is_integrable_on ['a,b'] & f1 | ['a,b'] is bounded & integral (f1,a,b) = (b - a) * e1 ) by Th29, A1, A2; integral (f1,a,b) = integral (f,a,b) by A3, A1, Th45; hence ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e ) by A3, Th43, A1, Th34, REAL_NS1:3; ::_thesis: verum end; theorem Th52: :: INTEGR19:52 for n being Element of NAT for a, b, c, d being real number for E being Point of (REAL-NS n) for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds f . x = E ) & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = (d - c) * E proof let n be Element of NAT ; ::_thesis: for a, b, c, d being real number for E being Point of (REAL-NS n) for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds f . x = E ) & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = (d - c) * E let a, b, c, d be real number ; ::_thesis: for E being Point of (REAL-NS n) for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds f . x = E ) & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = (d - c) * E let e be Point of (REAL-NS n); ::_thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds f . x = e ) & c in ['a,b'] & d in ['a,b'] holds integral (f,c,d) = (d - c) * e let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds f . x = e ) & c in ['a,b'] & d in ['a,b'] implies integral (f,c,d) = (d - c) * e ) assume A1: ( a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds f . x = e ) & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral (f,c,d) = (d - c) * e reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def_4; reconsider e1 = e as Element of REAL n by REAL_NS1:def_4; A2: for x being real number st x in ['a,b'] holds f1 . x = e1 by A1; A3: ( f1 is_integrable_on ['a,b'] & f1 | ['a,b'] is bounded & integral (f1,a,b) = (b - a) * e1 ) by Th29, A1, A2; A4: integral (f1,c,d) = (d - c) * e1 by Th30, A1; ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A5: ( a <= c & d <= b & a <= d & c <= b ) by A1, XXREAL_1:1; percases ( c <= d or not c <= d ) ; supposeA6: c <= d ; ::_thesis: integral (f,c,d) = (d - c) * e A7: ( ['c,d'] c= dom f1 & f1 | ['c,d'] is bounded & f1 is_integrable_on ['c,d'] ) by A3, A1, Th9, A5, A6, Th2; integral (f1,c,d) = integral (f,c,d) by A7, A6, Th45; hence integral (f,c,d) = (d - c) * e by A4, REAL_NS1:3; ::_thesis: verum end; supposeA8: not c <= d ; ::_thesis: integral (f,c,d) = (d - c) * e A9: ( ['d,c'] c= dom f1 & f1 | ['d,c'] is bounded & f1 is_integrable_on ['d,c'] ) by A3, A1, Th9, A5, A8, Th2; A10: integral (f1,d,c) = integral (f,d,c) by A9, A8, Th45; integral (f1,c,d) = - (integral (f1,d,c)) by Th33 .= - (integral (f,d,c)) by A10, REAL_NS1:4 .= integral (f,c,d) by A8, A9, Th47 ; hence integral (f,c,d) = (d - c) * e by A4, REAL_NS1:3; ::_thesis: verum end; end; end; theorem Th53: :: INTEGR19:53 for n being Element of NAT for a, b, c, d being real number for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) proof let n be Element of NAT ; ::_thesis: for a, b, c, d being real number for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) ) assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A2: ( a in ['a,b'] & b in ['a,b'] ) by A1, XXREAL_1:1; reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def_4; A3: f1 | ['a,b'] is bounded by A1, Th34; A4: f1 is_integrable_on ['a,b'] by Th43, A3, A1; A5: integral (f1,a,d) = (integral (f1,a,c)) + (integral (f1,c,d)) by A3, A4, A1, Th31; A6: integral (f,a,d) = integral (f1,a,d) by A2, Th48, A1; A7: integral (f,a,c) = integral (f1,a,c) by A2, Th48, A1; integral (f,c,d) = integral (f1,c,d) by Th48, A1; hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A7, A5, A6, REAL_NS1:2; ::_thesis: verum end; theorem Th54: :: INTEGR19:54 for n being Element of NAT for a, b, c, d, e being real number for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds ||.(f /. x).|| <= e ) holds ||.(integral (f,c,d)).|| <= (n * e) * (abs (d - c)) proof let n be Element of NAT ; ::_thesis: for a, b, c, d, e being real number for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds ||.(f /. x).|| <= e ) holds ||.(integral (f,c,d)).|| <= (n * e) * (abs (d - c)) let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds ||.(f /. x).|| <= e ) holds ||.(integral (f,c,d)).|| <= (n * e) * (abs (d - c)) let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds ||.(f /. x).|| <= e ) implies ||.(integral (f,c,d)).|| <= (n * e) * (abs (d - c)) ) assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds ||.(f /. x).|| <= e ) ) ; ::_thesis: ||.(integral (f,c,d)).|| <= (n * e) * (abs (d - c)) reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def_4; A2: f1 | ['a,b'] is bounded by A1, Th34; A3: f1 is_integrable_on ['a,b'] by Th43, A2, A1; for x being real number st x in ['(min (c,d)),(max (c,d))'] holds |.(f1 /. x).| <= e proof let x be real number ; ::_thesis: ( x in ['(min (c,d)),(max (c,d))'] implies |.(f1 /. x).| <= e ) assume A4: x in ['(min (c,d)),(max (c,d))'] ; ::_thesis: |.(f1 /. x).| <= e then A5: ||.(f /. x).|| <= e by A1; ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A1, Lm2; then A6: x in ['a,b'] by A4; then f /. x = f . x by A1, PARTFUN1:def_6 .= f1 /. x by A6, A1, PARTFUN1:def_6 ; hence |.(f1 /. x).| <= e by A5, REAL_NS1:1; ::_thesis: verum end; then |.(integral (f1,c,d)).| <= (n * e) * (abs (d - c)) by A1, A2, A3, Th32; hence ||.(integral (f,c,d)).|| <= (n * e) * (abs (d - c)) by Th48, A1, REAL_NS1:1; ::_thesis: verum end; begin Lm17: for a being real number for X being RealNormSpace for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / (abs a) proof let a be real number ; ::_thesis: for X being RealNormSpace for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / (abs a) let X be RealNormSpace; ::_thesis: for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / (abs a) let x be Point of X; ::_thesis: ||.((a ") * x).|| = ||.x.|| / (abs a) thus ||.((a ") * x).|| = (abs (a ")) * ||.x.|| by NORMSP_1:def_1 .= ((abs a) ") * ||.x.|| by COMPLEX1:66 .= (1 / (abs a)) * ||.x.|| by XCMPLX_1:215 .= ||.x.|| / (abs a) by XCMPLX_1:99 ; ::_thesis: verum end; theorem Th55: :: INTEGR19:55 for a, b, x0 being real number for n being non empty Element of NAT for F, f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds ( F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) proof let a, b, x0 be real number ; ::_thesis: for n being non empty Element of NAT for F, f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds ( F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) let n be non empty Element of NAT ; ::_thesis: for F, f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds ( F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) let F, f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 implies ( F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) ) deffunc H1( set ) -> Element of the carrier of (REAL-NS n) = 0. (REAL-NS n); assume that A1: a <= b and A2: f is_integrable_on ['a,b'] and A3: f | ['a,b'] is bounded and A4: ['a,b'] c= dom f and A5: ].a,b.[ c= dom F and A6: for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) and A7: x0 in ].a,b.[ and A8: f is_continuous_in x0 ; ::_thesis: ( F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) defpred S1[ set ] means x0 + (R_id $1) in ].a,b.[; deffunc H2( Element of REAL ) -> Element of the carrier of (REAL-NS n) = $1 * (f /. x0); consider L being Function of REAL,(REAL-NS n) such that A9: for h being Real holds L . h = H2(h) from FUNCT_2:sch_4(); reconsider L = L as LinearFunc of (REAL-NS n) by A9, NDIFF_3:def_2; deffunc H3( set ) -> Element of the carrier of (REAL-NS n) = ((F /. (x0 + (R_id $1))) - (F /. x0)) - (L . (R_id $1)); consider R being Function such that A10: ( dom R = REAL & ( for x being set st x in REAL holds ( ( S1[x] implies R . x = H3(x) ) & ( not S1[x] implies R . x = H1(x) ) ) ) ) from PARTFUN1:sch_1(); rng R c= the carrier of (REAL-NS n) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng R or y in the carrier of (REAL-NS n) ) assume y in rng R ; ::_thesis: y in the carrier of (REAL-NS n) then consider x being set such that A11: x in dom R and A12: y = R . x by FUNCT_1:def_3; A13: ( not S1[x] implies R . x = H1(x) ) by A10, A11; ( S1[x] implies R . x = H3(x) ) by A10, A11; hence y in the carrier of (REAL-NS n) by A12, A13; ::_thesis: verum end; then reconsider R = R as PartFunc of REAL,(REAL-NS n) by A10, RELSET_1:4; A14: R is total by A10, PARTFUN1:def_2; A15: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; A16: for h being non-zero 0 -convergent Real_Sequence holds ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. (REAL-NS n) ) proof let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. (REAL-NS n) ) set Z0 = 0. (REAL-NS n); A17: for e being Real st 0 < e holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e proof set g = REAL --> (f /. x0); let e0 be Real; ::_thesis: ( 0 < e0 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 ) set e = (e0 / 2) / n; A18: ( h is convergent & lim h = 0 ) ; assume A19: 0 < e0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 then 0 < e0 / 2 by XREAL_1:215; then 0 < (e0 / 2) / n by XREAL_1:139; then consider p being real number such that A20: 0 < p and A21: for t being real number st t in dom f & abs (t - x0) < p holds ||.((f /. t) - (f /. x0)).|| < (e0 / 2) / n by A8, NFCONT_3:8; A22: 0 < p / 2 by A20, XREAL_1:215; A23: p / 2 < p by A20, XREAL_1:216; consider N being Neighbourhood of x0 such that A24: N c= ].a,b.[ by A7, RCOMP_1:18; consider q being real number such that A25: 0 < q and A26: N = ].(x0 - q),(x0 + q).[ by RCOMP_1:def_6; A27: q / 2 < q by A25, XREAL_1:216; set r = min ((p / 2),(q / 2)); 0 < q / 2 by A25, XREAL_1:215; then 0 < min ((p / 2),(q / 2)) by A22, XXREAL_0:15; then consider n0 being Element of NAT such that A28: for m being Element of NAT st n0 <= m holds abs ((h . m) - 0) < min ((p / 2),(q / 2)) by A18, SEQ_2:def_7; take n0 ; ::_thesis: for m being Element of NAT st n0 <= m holds ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 let m be Element of NAT ; ::_thesis: ( n0 <= m implies ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 ) min ((p / 2),(q / 2)) <= q / 2 by XXREAL_0:17; then A29: ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ c= ].(x0 - q),(x0 + q).[ by A27, INTEGRA6:2, XXREAL_0:2; assume n0 <= m ; ::_thesis: ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 then A30: abs ((h . m) - 0) < min ((p / 2),(q / 2)) by A28; then abs ((x0 + (h . m)) - x0) < min ((p / 2),(q / 2)) ; then x0 + (h . m) in ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ by RCOMP_1:1; then A31: x0 + (h . m) in ].(x0 - q),(x0 + q).[ by A29; then A32: x0 + (h . m) in ].a,b.[ by A24, A26; then x0 + (R_id (h . m)) in ].a,b.[ by RSSPACE:def_3; then R . (h . m) = ((F /. (x0 + (R_id (h . m)))) - (F /. x0)) - (L . (R_id (h . m))) by A10; then R . (h . m) = ((F /. (x0 + (h . m))) - (F /. x0)) - (L . (R_id (h . m))) by RSSPACE:def_3; then A33: R . (h . m) = ((F /. (x0 + (h . m))) - (F /. x0)) - (L . (h . m)) by RSSPACE:def_3; A34: F /. x0 = F . x0 by A7, A5, PARTFUN1:def_6 .= integral (f,a,x0) by A6, A7 ; F /. (x0 + (h . m)) = F . (x0 + (h . m)) by A32, A5, PARTFUN1:def_6 .= integral (f,a,(x0 + (h . m))) by A6, A24, A26, A31 ; then A35: R . (h . m) = ((integral (f,a,(x0 + (h . m)))) - (integral (f,a,x0))) - ((h . m) * (f /. x0)) by A34, A9, A33; A36: dom (REAL --> (f /. x0)) = REAL by FUNCT_2:def_1; then ['a,b'] /\ ['a,b'] c= (dom f) /\ (dom (REAL --> (f /. x0))) by A4, XBOOLE_1:27; then A37: ['a,b'] c= dom (f - (REAL --> (f /. x0))) by VFUNCT_1:def_2; A38: ].a,b.[ c= [.a,b.] by XXREAL_1:25; then A39: integral (f,a,(x0 + (h . m))) = (integral (f,a,x0)) + (integral (f,x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A15, A32, Th53; A40: min ((p / 2),(q / 2)) <= p / 2 by XXREAL_0:17; A41: for x being real number st x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] holds ||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n proof let x be real number ; ::_thesis: ( x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] implies ||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n ) A42: ( min (x0,(x0 + (h . m))) <= x0 & x0 <= max (x0,(x0 + (h . m))) ) by XXREAL_0:17, XXREAL_0:25; assume x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] ; ::_thesis: ||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n then A43: x in [.(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m)))).] by A42, INTEGRA5:def_3, XXREAL_0:2; abs (x - x0) <= abs (h . m) proof percases ( x0 <= x0 + (h . m) or not x0 <= x0 + (h . m) ) ; suppose x0 <= x0 + (h . m) ; ::_thesis: abs (x - x0) <= abs (h . m) then ( x0 = min (x0,(x0 + (h . m))) & x0 + (h . m) = max (x0,(x0 + (h . m))) ) by XXREAL_0:def_9, XXREAL_0:def_10; then A44: ex z being Real st ( x = z & x0 <= z & z <= x0 + (h . m) ) by A43; then 0 <= x - x0 by XREAL_1:48; then A45: abs (x - x0) = x - x0 by ABSVALUE:def_1; A46: x - x0 <= (x0 + (h . m)) - x0 by A44, XREAL_1:9; then 0 <= h . m by A44, XREAL_1:48; hence abs (x - x0) <= abs (h . m) by A46, A45, ABSVALUE:def_1; ::_thesis: verum end; supposeA47: not x0 <= x0 + (h . m) ; ::_thesis: abs (x - x0) <= abs (h . m) then ( x0 = max (x0,(x0 + (h . m))) & x0 + (h . m) = min (x0,(x0 + (h . m))) ) by XXREAL_0:def_9, XXREAL_0:def_10; then A48: ex z being Real st ( x = z & x0 + (h . m) <= z & z <= x0 ) by A43; then A49: (x0 + (h . m)) - x0 <= x - x0 by XREAL_1:9; percases ( x - x0 <> 0 or x - x0 = 0 ) ; supposeA50: x - x0 <> 0 ; ::_thesis: abs (x - x0) <= abs (h . m) (x0 + (h . m)) - x0 < x0 - x0 by A47, XREAL_1:14; then A51: abs (h . m) = - (h . m) by ABSVALUE:def_1; x - x0 < 0 by A48, A50, XREAL_1:47; then abs (x - x0) = - (x - x0) by ABSVALUE:def_1; hence abs (x - x0) <= abs (h . m) by A49, A51, XREAL_1:24; ::_thesis: verum end; suppose x - x0 = 0 ; ::_thesis: abs (x - x0) <= abs (h . m) then abs (x - x0) = 0 by ABSVALUE:def_1; hence abs (x - x0) <= abs (h . m) by COMPLEX1:46; ::_thesis: verum end; end; end; end; end; then A52: abs (x - x0) < min ((p / 2),(q / 2)) by A30, XXREAL_0:2; then x in ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ by RCOMP_1:1; then x in ].(x0 - q),(x0 + q).[ by A29; then x in ].a,b.[ by A24, A26; then A53: x in [.a,b.] by A38; reconsider xx = x as Real by XREAL_0:def_1; abs (x - x0) < p / 2 by A40, A52, XXREAL_0:2; then abs (x - x0) < p by A23, XXREAL_0:2; then ||.((f /. x) - (f /. x0)).|| <= (e0 / 2) / n by A4, A15, A21, A53; then ||.((f /. x) - ((REAL --> (f /. x0)) /. xx)).|| <= (e0 / 2) / n by FUNCOP_1:7; hence ||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n by A15, A37, A53, VFUNCT_1:def_2; ::_thesis: verum end; A54: for x being real number st x in ['a,b'] holds (REAL --> (f /. x0)) . x = f /. x0 by FUNCOP_1:7; then A55: (REAL --> (f /. x0)) | ['a,b'] is bounded by A1, A36, Th51; then A56: (f - (REAL --> (f /. x0))) | (['a,b'] /\ ['a,b']) is bounded by A3, Th35; rng h c= dom R by A10; then ((h . m) ") * (R /. (h . m)) = ((h . m) ") * ((R /* h) . m) by FUNCT_2:109; then ((h . m) ") * (R /. (h . m)) = ((h ") . m) * ((R /* h) . m) by VALUED_1:10; then A57: ((h . m) ") * (R /. (h . m)) = ((h ") (#) (R /* h)) . m by NDIFF_1:def_2; dom h = NAT by FUNCT_2:def_1; then h . m <> 0 ; then A58: 0 < abs (h . m) by COMPLEX1:47; A59: REAL --> (f /. x0) is_integrable_on ['a,b'] by A1, A36, A54, Th51; then A60: ||.(integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m)))).|| <= (n * ((e0 / 2) / n)) * (abs ((x0 + (h . m)) - x0)) by A1, A7, A15, A38, A32, A56, A37, A41, Th54, A2, A4, A36, INTEGR18:15; A61: integral ((REAL --> (f /. x0)),x0,(x0 + (h . m))) = ((x0 + (h . m)) - x0) * (f /. x0) by A1, A7, A15, A38, A32, A36, A54, Th52 .= (h . m) * (f /. x0) ; A62: integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m))) = (integral (f,x0,(x0 + (h . m)))) - (integral ((REAL --> (f /. x0)),x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A15, A38, A32, A36, A59, A55, Th50; R . (h . m) = ((integral (f,x0,(x0 + (h . m)))) + ((integral (f,a,x0)) - (integral (f,a,x0)))) - ((h . m) * (f /. x0)) by A35, A39, RLVECT_1:28 .= ((integral (f,x0,(x0 + (h . m)))) + (0. (REAL-NS n))) - ((h . m) * (f /. x0)) by RLVECT_1:15 .= (integral (f,x0,(x0 + (h . m)))) - (integral ((REAL --> (f /. x0)),x0,(x0 + (h . m)))) by A61, RLVECT_1:def_4 ; then R /. (h . m) = integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m))) by A62, A10, PARTFUN1:def_6; then ( ||.(((h . m) ") * (R /. (h . m))).|| = ||.(R /. (h . m)).|| / (abs (h . m)) & ||.(R /. (h . m)).|| / (abs (h . m)) <= ((n * ((e0 / 2) / n)) * (abs (h . m))) / (abs (h . m)) ) by A60, A58, Lm17, XREAL_1:72; then ||.(((h . m) ") * (R /. (h . m))).|| <= n * ((e0 / 2) / n) by A58, XCMPLX_1:89; then A63: ||.(((h . m) ") * (R /. (h . m))).|| <= e0 / 2 by XCMPLX_1:87; e0 / 2 < e0 by A19, XREAL_1:216; then ||.(((h ") (#) (R /* h)) . m).|| < e0 by A63, A57, XXREAL_0:2; hence ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 by RLVECT_1:13; ::_thesis: verum end; hence (h ") (#) (R /* h) is convergent by NORMSP_1:def_6; ::_thesis: lim ((h ") (#) (R /* h)) = 0. (REAL-NS n) hence lim ((h ") (#) (R /* h)) = 0. (REAL-NS n) by A17, NORMSP_1:def_7; ::_thesis: verum end; consider N being Neighbourhood of x0 such that A64: N c= ].a,b.[ by A7, RCOMP_1:18; reconsider R = R as RestFunc of (REAL-NS n) by A14, A16, NDIFF_3:def_1; A65: for x being Real st x in N holds (F /. x) - (F /. x0) = (L . (x - x0)) + (R /. (x - x0)) proof let x be Real; ::_thesis: ( x in N implies (F /. x) - (F /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) assume x in N ; ::_thesis: (F /. x) - (F /. x0) = (L . (x - x0)) + (R /. (x - x0)) then x0 + (x - x0) in N ; then x0 + (R_id (x - x0)) in N by RSSPACE:def_3; then ( x0 + (R_id (x - x0)) = x0 + (x - x0) & R . (x - x0) = H3(x - x0) ) by A10, A64, RSSPACE:def_3; then R /. (x - x0) = ((F /. x) - (F /. x0)) - (L . (x - x0)) by A10, PARTFUN1:def_6; then (R /. (x - x0)) + (L . (x - x0)) = ((F /. x) - (F /. x0)) - ((L . (x - x0)) - (L . (x - x0))) by RLVECT_1:29 .= ((F /. x) - (F /. x0)) - (0. (REAL-NS n)) by RLVECT_1:15 .= (F /. x) - (F /. x0) by RLVECT_1:13 ; hence (F /. x) - (F /. x0) = (L . (x - x0)) + (R /. (x - x0)) ; ::_thesis: verum end; A66: N c= dom F by A5, A64, XBOOLE_1:1; hence A67: F is_differentiable_in x0 by A65, NDIFF_3:def_3; ::_thesis: diff (F,x0) = f /. x0 reconsider N1 = 1 as Real ; L . 1 = N1 * (f /. x0) by A9 .= f /. x0 by RLVECT_1:def_8 ; hence diff (F,x0) = f /. x0 by A66, A65, A67, NDIFF_3:def_4; ::_thesis: verum end; Lm18: for n being Element of NAT for a, b being real number for f being PartFunc of REAL,(REAL-NS n) ex F being PartFunc of REAL,(REAL-NS n) st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) proof let n be Element of NAT ; ::_thesis: for a, b being real number for f being PartFunc of REAL,(REAL-NS n) ex F being PartFunc of REAL,(REAL-NS n) st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) let a, b be real number ; ::_thesis: for f being PartFunc of REAL,(REAL-NS n) ex F being PartFunc of REAL,(REAL-NS n) st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) deffunc H1( real number ) -> Element of the carrier of (REAL-NS n) = 0. (REAL-NS n); let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ex F being PartFunc of REAL,(REAL-NS n) st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) defpred S1[ set ] means $1 in ].a,b.[; deffunc H2( real number ) -> Element of the carrier of (REAL-NS n) = integral (f,a,$1); consider F being Function such that A1: ( dom F = REAL & ( for x being Element of REAL holds ( ( S1[x] implies F . x = H2(x) ) & ( not S1[x] implies F . x = H1(x) ) ) ) ) from PARTFUN1:sch_4(); now__::_thesis:_for_y_being_set_st_y_in_rng_F_holds_ y_in_the_carrier_of_(REAL-NS_n) let y be set ; ::_thesis: ( y in rng F implies y in the carrier of (REAL-NS n) ) assume y in rng F ; ::_thesis: y in the carrier of (REAL-NS n) then consider x being set such that A2: x in dom F and A3: y = F . x by FUNCT_1:def_3; reconsider x = x as Element of REAL by A1, A2; A4: now__::_thesis:_(_not_x_in_].a,b.[_implies_y_in_the_carrier_of_(REAL-NS_n)_) assume not x in ].a,b.[ ; ::_thesis: y in the carrier of (REAL-NS n) then F . x = 0. (REAL-NS n) by A1; hence y in the carrier of (REAL-NS n) by A3; ::_thesis: verum end; now__::_thesis:_(_x_in_].a,b.[_implies_y_in_the_carrier_of_(REAL-NS_n)_) assume x in ].a,b.[ ; ::_thesis: y in the carrier of (REAL-NS n) then F . x = integral (f,a,x) by A1; hence y in the carrier of (REAL-NS n) by A3; ::_thesis: verum end; hence y in the carrier of (REAL-NS n) by A4; ::_thesis: verum end; then rng F c= the carrier of (REAL-NS n) by TARSKI:def_3; then reconsider F = F as PartFunc of REAL,(REAL-NS n) by A1, RELSET_1:4; take F ; ::_thesis: ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) thus ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) by A1; ::_thesis: verum end; theorem :: INTEGR19:56 for a, b, x0 being real number for n being non empty Element of NAT for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds ex F being PartFunc of REAL,(REAL-NS n) st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) proof let a, b, x0 be real number ; ::_thesis: for n being non empty Element of NAT for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds ex F being PartFunc of REAL,(REAL-NS n) st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds ex F being PartFunc of REAL,(REAL-NS n) st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 implies ex F being PartFunc of REAL,(REAL-NS n) st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) ) consider F being PartFunc of REAL,(REAL-NS n) such that A1: ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) by Lm18; assume ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 ) ; ::_thesis: ex F being PartFunc of REAL,(REAL-NS n) st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) then ( F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) by A1, Th55; hence ex F being PartFunc of REAL,(REAL-NS n) st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) by A1; ::_thesis: verum end;