:: Riemann Integral of Functions from $\mathbbbR$ into $n$-dimensional Real Normed Space :: by Keiichi Miyajima , Artur Korni{\l}owicz and Yasunari Shidama :: :: Received October 27, 2011 :: Copyright (c) 2011-2012 Association of Mizar Users 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'] ) proofend; 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 proofend; 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'] proofend; 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 proofend; 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) proofend; 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) proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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)) proofend; 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)) ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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.| proofend; 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 proofend; 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 proofend; 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) proofend; 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) proofend; 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) ) proofend; 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))) ) proofend; 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) ) proofend; 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) proofend; 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)) proofend; 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) proofend; 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) proofend; 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)) proofend; 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)) proofend; 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)) proofend; 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)) proofend; 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 ) proofend; 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 proofend; 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)) proofend; 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)) proofend; 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)) proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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) proofend; 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 ) proofend; 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) proofend; 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 ) ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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) ) proofend; 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) proofend; 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)) ) proofend; 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)) proofend; 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) proofend; 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)) proofend; 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)) proofend; 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 ) proofend; 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 proofend; 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)) proofend; 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)) proofend; begin Lm17: for a being real number for X being RealNormSpace for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / (abs a) proofend; 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 ) proofend; 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) ) ) proofend; 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 ) proofend;