:: by Keiichi Miyajima , Artur Korni{\l}owicz and Yasunari Shidama

::

:: Received October 27, 2011

:: Copyright (c) 2011-2018 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'] )

( 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

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

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)

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)

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 )

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 )

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)) )

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 )

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 )

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 )

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 )

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 )

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 )

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

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 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.|

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

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

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)

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)

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))) )

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;

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;

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))

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))

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))

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))

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 )

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

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))

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).|

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))

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;

:: 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 );

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 )

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 )

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 )

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)

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 )

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)

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 ) )

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 )

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 )

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 )

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) )

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)

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)) )

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))

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)

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))

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))

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 )

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

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))

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).|

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 )

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 )

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;