:: 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-2021 Association of Mizar Users

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, b, c being Real st a <= c & c <= b holds
( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] )

proof end;

theorem Th2: :: INTEGR19:2

for X being set
for a, b, c, d being Real st a <= c & c <= d & d <= b & ['a,b'] c= X holds
['c,d'] c= X

proof end;

Lm2: for a, b, c, d being Real st a <= b & c in ['a,b'] & d in ['a,b'] holds
['(min (c,d)),(max (c,d))'] c= ['a,b']

proof end;

theorem Th3: :: INTEGR19:3

for X being set
for a, b, c, d being Real 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 end;

theorem Th4: :: INTEGR19:4

for n being Element of NAT
for a, b, c, d being Real
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 end;

theorem Th5: :: INTEGR19:5

for n being Element of NAT
for a, b, c, d being Real
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 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 end;

theorem Th6: :: INTEGR19:6

for a, b, c, d, r being Real
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 end;

theorem :: INTEGR19:7

for a, b, c, d being Real
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 end;

Lm4: for a, b, c, d, e being Real
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 st x in ['(min (c,d)),(max (c,d))'] holds
|.(f . x).| <= e ) holds
|.(integral (f,c,d)).| <= e * |.(d - c).|

proof 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
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 end;

theorem Th9: :: INTEGR19:9

for n being Element of NAT
for a, b, c, d being Real
for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )

proof end;

theorem Th10: :: INTEGR19:10

for n being Element of NAT
for a, b, c, d being Real
for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded )

proof end;

theorem Th11: :: INTEGR19:11

for n being Element of NAT
for a, b, c, d, r being Real
for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded )

proof end;

theorem Th12: :: INTEGR19:12

for n being Element of NAT
for a, b, c, d being Real
for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( - f is_integrable_on ['c,d'] & (- f) | ['c,d'] is bounded )

proof end;

theorem Th13: :: INTEGR19:13

for n being Element of NAT
for a, b, c, d being Real
for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded )

proof end;

theorem Th14: :: INTEGR19:14

for A being non empty closed_interval Subset of REAL
for n being non zero Element of NAT
for f being Function of A,(REAL n) holds
( f is bounded iff |.f.| is bounded )

proof 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 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 end;

Lm8: for A being non empty closed_interval Subset of REAL
for n being non zero 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 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 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 ;

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 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 end;

theorem Th19: :: INTEGR19:19

for A being non empty closed_interval Subset of REAL
for n being non zero 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 end;

theorem Th20: :: INTEGR19:20

for A being non empty closed_interval Subset of REAL
for n being non zero 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 end;

theorem Th21: :: INTEGR19:21

for a, b being Real
for n being non zero 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 end;

Lm10: for a, b, c, d being Real
for n being non zero 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 end;

theorem Th22: :: INTEGR19:22

for a, b, c, d being Real
for n being non zero 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 end;

Lm11: for a, b, c, d being Real
for n being non zero 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 end;

Lm12: for a, b, c, d being Real
for n being non zero 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 end;

theorem :: INTEGR19:23

for a, b, c, d being Real
for n being non zero 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
for n being non zero 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 st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= e * |.(d - c).|

proof end;

Lm14: for a, b, c, d, e being Real
for n being non zero 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 st x in ['c,d'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= e * (d - c)

proof end;

Lm15: for a, b, c, d, e being Real
for n being non zero 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 st x in ['c,d'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,d,c)).| <= e * (d - c)

proof end;

theorem :: INTEGR19:24

for a, b, c, d, e being Real
for n being non zero 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 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
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 end;

theorem Th26: :: INTEGR19:26

for n being Element of NAT
for a, b, c, d being Real
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 end;

theorem Th27: :: INTEGR19:27

for n being Element of NAT
for a, b, c, d being Real
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 end;

theorem Th28: :: INTEGR19:28

for n being Element of NAT
for a, b, c, d being Real
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 end;

theorem Th29: :: INTEGR19:29

for n being Element of NAT
for a, b being Real
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 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 end;

theorem Th30: :: INTEGR19:30

for n being Element of NAT
for a, b, c, d being Real
for f being PartFunc of REAL,(REAL n)
for E being Element of REAL n st a <= b & ( for x being Real 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 end;

theorem Th31: :: INTEGR19:31

for n being Element of NAT
for a, b, c, d being Real
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 end;

theorem Th32: :: INTEGR19:32

for n being Element of NAT
for a, b, c, d, e being Real
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 st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= (n * e) * |.(d - c).|

proof end;

theorem Th33: :: INTEGR19:33

for n being Element of NAT
for a, b being Real
for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b))

proof end;

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 end;

definition

let R be RealNormSpace;
let X be non empty set ;
let g be PartFunc of X,R;

attr g is bounded means :: INTEGR19:def 1
ex r being Real st
for y being set st y in dom g holds
||.(g /. y).|| < r;

end;

:: deftheorem 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 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 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 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 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 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 sequence of ((REAL n) *)
for q being sequence of ( 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 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 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 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 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 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 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 end;

theorem Th45: :: INTEGR19:45

for n being Element of NAT
for a, b being Real
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 end;

theorem :: INTEGR19:46

for n being Element of NAT
for a, b being Real
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 end;

theorem Th47: :: INTEGR19:47

for n being Element of NAT
for a, b being Real
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 end;

theorem Th48: :: INTEGR19:48

for n being Element of NAT
for a, b, c, d being Real
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 end;

theorem :: INTEGR19:49

for n being Element of NAT
for a, b, c, d being Real
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 end;

theorem Th50: :: INTEGR19:50

for n being Element of NAT
for a, b, c, d being Real
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 end;

theorem Th51: :: INTEGR19:51

for n being Element of NAT
for a, b being Real
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 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 end;

theorem Th52: :: INTEGR19:52

for n being Element of NAT
for a, b, c, d being Real
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 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 end;

theorem Th53: :: INTEGR19:53

for n being Element of NAT
for a, b, c, d being Real
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 end;

theorem Th54: :: INTEGR19:54

for n being Element of NAT
for a, b, c, d, e being Real
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 st x in ['(min (c,d)),(max (c,d))'] holds
||.(f /. x).|| <= e ) holds
||.(integral (f,c,d)).|| <= (n * e) * |.(d - c).|

proof end;

Lm17: for a being Real
for X being RealNormSpace
for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / |.a.|

proof end;

theorem Th55: :: INTEGR19:55

for a, b, x0 being Real
for n being non zero 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 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 end;

Lm18: for n being Element of NAT
for a, b being Real
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 st x in ].a,b.[ holds
F . x = integral (f,a,x) ) )

proof end;

theorem :: INTEGR19:56

for a, b, x0 being Real
for n being non zero 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 st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 )

proof end;