:: Gauge Integral
:: by Roland Coghetto
::
:: Received September 3, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


theorem Th01: :: COUSIN2:1
for a, b, c being Real st a - b <= c & b <= a holds
|.(b - a).| <= c
proof end;

theorem Th02: :: COUSIN2:2
for a, b, c being Real st b - a <= c & a <= b holds
|.(b - a).| <= c
proof end;

Lm01: for a, b, c, d being Real st a <= b + c & b <= d holds
a <= d + c
proof end;

Lm02: for a, b, c, d being Real st a < b + c & b - c < d holds
a - d < 2 * c
proof end;

theorem Th03: :: COUSIN2:3
for a, b, c, d, e being Real st a <= b & b <= c & |.(a - d).| <= e & |.(c - d).| <= e holds
|.(b - d).| <= e
proof end;

theorem Th04: :: COUSIN2:4
for a, b being Real st ( for c being Real st 0 < c holds
|.(a - b).| <= c ) holds
a = b
proof end;

theorem Th05: :: COUSIN2:5
for e being Real
for b, c, d being non negative Real st d < e / ((2 * b) * |.c.|) holds
( b is positive & c is positive )
proof end;

theorem Th06: :: COUSIN2:6
for a, b being Real st a <> 0 holds
a * (b / (2 * a)) = b / 2
proof end;

theorem Th07: :: COUSIN2:7
for a, e being Real
for b, c, d being non negative Real st a <= (b * c) * d & d < e / ((2 * b) * |.c.|) holds
a <= e / 2
proof end;

definition
let X be non empty set ;
let f, g be Function of X,REAL;
func min (f,g) -> Function of X,REAL means :DEFM1: :: COUSIN2:def 1
 for x being Element of X holds it . x = min ((f . x),(g . x));
existence
ex b1 being Function of X,REAL st
for x being Element of X holds b1 . x = min ((f . x),(g . x))
proof end;
uniqueness
for b1, b2 being Function of X,REAL st ( for x being Element of X holds b1 . x = min ((f . x),(g . x)) ) & ( for x being Element of X holds b2 . x = min ((f . x),(g . x)) ) holds
b1 = b2
proof end;
commutativity
for b1, f, g being Function of X,REAL st ( for x being Element of X holds b1 . x = min ((f . x),(g . x)) ) holds
for x being Element of X holds b1 . x = min ((g . x),(f . x)) ;
func max (f,g) -> Function of X,REAL means :DEFM2: :: COUSIN2:def 2
 for x being Element of X holds it . x = max ((f . x),(g . x));
existence
ex b1 being Function of X,REAL st
for x being Element of X holds b1 . x = max ((f . x),(g . x))
proof end;
uniqueness
for b1, b2 being Function of X,REAL st ( for x being Element of X holds b1 . x = max ((f . x),(g . x)) ) & ( for x being Element of X holds b2 . x = max ((f . x),(g . x)) ) holds
b1 = b2
proof end;
commutativity
for b1, f, g being Function of X,REAL st ( for x being Element of X holds b1 . x = max ((f . x),(g . x)) ) holds
for x being Element of X holds b1 . x = max ((g . x),(f . x)) ;
end;

:: deftheorem DEFM1 defines min COUSIN2:def 1 :
for X being non empty set
for f, g, b4 being Function of X,REAL holds
( b4 = min (f,g) iff for x being Element of X holds b4 . x = min ((f . x),(g . x)) );

:: deftheorem DEFM2 defines max COUSIN2:def 2 :
for X being non empty set
for f, g, b4 being Function of X,REAL holds
( b4 = max (f,g) iff for x being Element of X holds b4 . x = max ((f . x),(g . x)) );

registration
let X be non empty set ;
let f, g be positive-yielding Function of X,REAL;
cluster min (f,g) -> positive-yielding ;
coherence
min (f,g) is positive-yielding
proof end;
end;

registration
let X be non empty set ;
let f, g be positive-yielding Function of X,REAL;
cluster max (f,g) -> positive-yielding ;
coherence
max (f,g) is positive-yielding
proof end;
end;

definition
let X be non empty set ;
let f, g be Function of X,REAL;
pred f <= g means :: COUSIN2:def 3
 for x being Element of X holds f . x <= g . x;
end;

:: deftheorem defines <= COUSIN2:def 3 :
for X being non empty set
for f, g being Function of X,REAL holds
( f <= g iff for x being Element of X holds f . x <= g . x );

theorem Th08: :: COUSIN2:8
for X being non empty set
for f, g being Function of X,REAL holds min (f,g) <= f
proof end;

Lm03: for X being non empty set st ex s being object st
for r being object st r in X holds
s = r holds
ex r being object st X = {r}
proof end;

theorem Th09: :: COUSIN2:9
for X being non empty real-membered set st ( for r being Real st r in X holds
upper_bound X = r ) holds
ex r being Real st X = {r}
proof end;

theorem :: COUSIN2:10
for X being non empty real-membered set st ( for r being Real st r in X holds
lower_bound X = r ) holds
ex r being Real st X = {r}
proof end;

theorem Th10: :: COUSIN2:11
for X being non empty real-membered bounded_below bounded_above set st upper_bound X = lower_bound X holds
ex r being Real st X = {r}
proof end;

theorem Th11: :: COUSIN2:12
for X, Y being set holds chi (X,Y) is Function of Y,REAL
proof end;

theorem :: COUSIN2:13
for r being Real
for s being ExtReal
for A being Subset of REAL st A c= ].r,s.[ holds
A is bounded_below
proof end;

theorem :: COUSIN2:14
for r being Real
for s being ExtReal
for A being Subset of REAL st A c= ].s,r.[ holds
A is bounded_above
proof end;

theorem Th12: :: COUSIN2:15
for a, b being Real
for f being real-valued Function st rng f c= [.a,b.] holds
f is bounded
proof end;

theorem Th13: :: COUSIN2:16
for a, b being Real st a <= b holds
{a,b} c= [.a,b.]
proof end;

theorem Th14: :: COUSIN2:17
for X, Y being set holds chi (X,Y) is bounded
proof end;

theorem Th15: :: COUSIN2:18
for X, Y being set st X misses Y holds
for x being Element of X holds (chi (Y,X)) . x = 0
proof end;

theorem Th16: :: COUSIN2:19
for Z being non empty set
for f being Function of Z,REAL holds
( f is constant iff ex r being Real st f = r (#) (chi (Z,Z)) )
proof end;

theorem Th17: :: COUSIN2:20
for X being set holds chi (X,X) is positive-yielding
proof end;

theorem Th18: :: COUSIN2:21
for I being non empty closed_interval Subset of REAL
for D being Division of I
for f being PartFunc of I,REAL st f is lower_integrable holds
lower_sum (f,D) <= lower_integral f
proof end;

theorem Th19: :: COUSIN2:22
for I being non empty closed_interval Subset of REAL
for D being Division of I
for f being PartFunc of I,REAL st f is upper_integrable holds
upper_integral f <= upper_sum (f,D)
proof end;

definition
let A be non empty closed_interval Subset of REAL;
func tagged_divs A -> set means :Def1: :: COUSIN2:def 4
 for x being set holds
( x in it iff x is tagged_division of A );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is tagged_division of A )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is tagged_division of A ) ) & ( for x being set holds
( x in b2 iff x is tagged_division of A ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines tagged_divs COUSIN2:def 4 :
for A being non empty closed_interval Subset of REAL
for b2 being set holds
( b2 = tagged_divs A iff for x being set holds
( x in b2 iff x is tagged_division of A ) );

registration
let A be non empty closed_interval Subset of REAL;
cluster tagged_divs A -> non empty ;
coherence
not tagged_divs A is empty
proof end;
end;

definition
let A be non empty closed_interval Subset of REAL;
let TD be tagged_division of A;
func tagged_of TD -> non empty non-decreasing FinSequence of REAL means :Def2: :: COUSIN2:def 5
 ex D being Division of A ex T being Element of set_of_tagged_Division D st
( it = T & TD = [D,T] );
existence
ex b1 being non empty non-decreasing FinSequence of REAL ex D being Division of A ex T being Element of set_of_tagged_Division D st
( b1 = T & TD = [D,T] )
proof end;
uniqueness
for b1, b2 being non empty non-decreasing FinSequence of REAL st ex D being Division of A ex T being Element of set_of_tagged_Division D st
( b1 = T & TD = [D,T] ) & ex D being Division of A ex T being Element of set_of_tagged_Division D st
( b2 = T & TD = [D,T] ) holds
b1 = b2 by XTUPLE_0:1;
end;

:: deftheorem Def2 defines tagged_of COUSIN2:def 5 :
for A being non empty closed_interval Subset of REAL
for TD being tagged_division of A
for b3 being non empty non-decreasing FinSequence of REAL holds
( b3 = tagged_of TD iff ex D being Division of A ex T being Element of set_of_tagged_Division D st
( b3 = T & TD = [D,T] ) );

theorem Th20: :: COUSIN2:23
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for D being Division of I
for T being Element of set_of_tagged_Division D st TD = [D,T] holds
( T = tagged_of TD & D = division_of TD )
proof end;

theorem Th21: :: COUSIN2:24
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I holds len (tagged_of TD) = len (division_of TD)
proof end;

definition
let A be non empty closed_interval Subset of REAL;
let TD be tagged_division of A;
func len TD -> Element of NAT equals :: COUSIN2:def 6
 len (division_of TD);
coherence
len (division_of TD) is Element of NAT ;
func dom TD -> set equals :: COUSIN2:def 7
 dom (division_of TD);
coherence
dom (division_of TD) is set ;
end;

:: deftheorem defines len COUSIN2:def 6 :
for A being non empty closed_interval Subset of REAL
for TD being tagged_division of A holds len TD = len (division_of TD);

:: deftheorem defines dom COUSIN2:def 7 :
for A being non empty closed_interval Subset of REAL
for TD being tagged_division of A holds dom TD = dom (division_of TD);

theorem Th22: :: COUSIN2:25
for I being non empty closed_interval Subset of REAL
for D being Division of I
for T being Element of set_of_tagged_Division D holds rng T c= I
proof end;

theorem Th23: :: COUSIN2:26
for I being non empty closed_interval Subset of REAL
for jauge1, jauge2 being positive-yielding Function of I,REAL
for TD being b2 -fine tagged_division of I st jauge1 <= jauge2 holds
TD is b3 -fine tagged_division of I
proof end;

definition
let I be non empty closed_interval Subset of REAL;
let f be PartFunc of I,REAL;
let TD be tagged_division of I;
func tagged_volume (f,TD) -> FinSequence of REAL means :Def4: :: COUSIN2:def 8
( len it = len TD & ( for i being Nat st i in dom TD holds
it . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len TD & ( for i being Nat st i in dom TD holds
b1 . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len TD & ( for i being Nat st i in dom TD holds
b1 . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) & len b2 = len TD & ( for i being Nat st i in dom TD holds
b2 . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines tagged_volume COUSIN2:def 8 :
for I being non empty closed_interval Subset of REAL
for f being PartFunc of I,REAL
for TD being tagged_division of I
for b4 being FinSequence of REAL holds
( b4 = tagged_volume (f,TD) iff ( len b4 = len TD & ( for i being Nat st i in dom TD holds
b4 . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) ) );

definition
let I be non empty closed_interval Subset of REAL;
let f be PartFunc of I,REAL;
let TD be tagged_division of I;
func tagged_sum (f,TD) -> Real equals :: COUSIN2:def 9
 Sum (tagged_volume (f,TD));
coherence
Sum (tagged_volume (f,TD)) is Real ;
end;

:: deftheorem defines tagged_sum COUSIN2:def 9 :
for I being non empty closed_interval Subset of REAL
for f being PartFunc of I,REAL
for TD being tagged_division of I holds tagged_sum (f,TD) = Sum (tagged_volume (f,TD));

theorem Th24: :: COUSIN2:27
for X, Y being set st Y c= X holds
chi (X,Y) = chi (Y,Y)
proof end;

theorem Th25: :: COUSIN2:28
for I being non empty closed_interval Subset of REAL st not I is empty & I is trivial holds
vol I = 0
proof end;

theorem Th26: :: COUSIN2:29
for I being non empty closed_interval Subset of REAL
for r being Real st I = {r} holds
for D being Division of I holds D = <*r*>
proof end;

Lm04: for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being Function of I,REAL st f = chi (I,I) holds
tagged_sum (f,TD) = vol I
proof end;

definition
let I be non empty closed_interval Subset of REAL;
let f be Function of I,REAL;
attr f is HK-integrable means :: COUSIN2:def 10
 ex J being Real st
for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - J).| <= epsilon;
end;

:: deftheorem defines HK-integrable COUSIN2:def 10 :
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL holds
( f is HK-integrable iff ex J being Real st
for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - J).| <= epsilon );

definition
let I be non empty closed_interval Subset of REAL;
let f be Function of I,REAL;
assume A1: f is HK-integrable ;
func HK-integral f -> Real means :DEFCC: :: COUSIN2:def 11
 for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - it).| <= epsilon;
existence
ex b1 being Real st
for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - b1).| <= epsilon by A1;
uniqueness
for b1, b2 being Real st ( for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - b1).| <= epsilon ) & ( for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - b2).| <= epsilon ) holds
b1 = b2
proof end;
end;

:: deftheorem DEFCC defines HK-integral COUSIN2:def 11 :
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st f is HK-integrable holds
for b3 being Real holds
( b3 = HK-integral f iff for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - b3).| <= epsilon );

theorem Th27: :: COUSIN2:30
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st I is trivial holds
( f is HK-integrable & HK-integral f = 0 )
proof end;

theorem Th28: :: COUSIN2:31
for A being Subset of REAL
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being Function of I,REAL st A misses I & f = chi (A,I) holds
tagged_sum (f,TD) = 0
proof end;

theorem Th29: :: COUSIN2:32
for A being Subset of REAL
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st A misses I & f = chi (A,I) holds
( f is HK-integrable & HK-integral f = 0 )
proof end;

theorem Th30: :: COUSIN2:33
for A being Subset of REAL
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st I c= A & f = chi (A,I) holds
( f is HK-integrable & HK-integral f = vol I )
proof end;

registration
let I be non empty closed_interval Subset of REAL;
cluster V1() V4(I) V5( REAL ) Function-like non empty total V55(I, REAL ) complex-valued ext-real-valued real-valued HK-integrable for Element of bool [:I,REAL:];
existence
ex b1 being Function of I,REAL st b1 is HK-integrable
proof end;
end;

theorem Th31: :: COUSIN2:34
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being HK-integrable Function of I,REAL
for r being Real
for i being Nat st i in dom TD holds
(tagged_volume ((r (#) f),TD)) . i = (r * (f . ((tagged_of TD) . i))) * (vol (divset ((division_of TD),i)))
proof end;

theorem Th32: :: COUSIN2:35
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being HK-integrable Function of I,REAL
for r being Real holds tagged_volume ((r (#) f),TD) = r * (tagged_volume (f,TD))
proof end;

theorem Th33: :: COUSIN2:36
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f, g being HK-integrable Function of I,REAL
for i being Nat st i in dom TD holds
(tagged_volume ((f + g),TD)) . i = ((f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) + ((g . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))))
proof end;

theorem Th34: :: COUSIN2:37
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f, g being HK-integrable Function of I,REAL holds tagged_volume ((f + g),TD) = (tagged_volume (f,TD)) + (tagged_volume (g,TD))
proof end;

theorem Th35: :: COUSIN2:38
for I being non empty closed_interval Subset of REAL
for f being HK-integrable Function of I,REAL
for r being Real st f is HK-integrable holds
( r (#) f is HK-integrable Function of I,REAL & HK-integral (r (#) f) = r * (HK-integral f) )
proof end;

theorem :: COUSIN2:39
for I being non empty closed_interval Subset of REAL
for f, g being HK-integrable Function of I,REAL holds
( f + g is HK-integrable Function of I,REAL & HK-integral (f + g) = (HK-integral f) + (HK-integral g) )
proof end;

theorem Th36: :: COUSIN2:40
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st f is constant holds
( f is HK-integrable & ex r being Real st
( f = r (#) (chi (I,I)) & HK-integral f = r * (vol I) ) )
proof end;

registration
let I be non empty closed_interval Subset of REAL;
cluster V1() V4(I) V5( REAL ) Function-like non empty total V55(I, REAL ) complex-valued ext-real-valued real-valued integrable for Element of bool [:I,REAL:];
existence
ex b1 being Function of I,REAL st b1 is integrable
proof end;
end;

registration
let X be non empty set ;
cluster V1() V4(X) V5( REAL ) Function-like non empty total V55(X, REAL ) complex-valued ext-real-valued real-valued bounded for Element of bool [:X,REAL:];
existence
ex b1 being Function of X,REAL st b1 is bounded
proof end;
end;

theorem Th37: :: COUSIN2:41
for I being non empty closed_interval Subset of REAL
for f being bounded Function of I,REAL holds
( |.((upper_bound (rng f)) - (lower_bound (rng f))).| = 0 iff f is constant )
proof end;

registration
let I be non empty closed_interval Subset of REAL;
cluster V1() V4(I) V5( REAL ) Function-like non empty total V55(I, REAL ) complex-valued ext-real-valued real-valued bounded integrable for Element of bool [:I,REAL:];
existence
ex b1 being integrable Function of I,REAL st b1 is bounded
proof end;
end;

theorem :: COUSIN2:42
for I being non empty closed_interval Subset of REAL
for f being PartFunc of I,REAL st f is upper_integrable holds
ex r being Real st
for D being Division of I holds r < upper_sum (f,D)
proof end;

theorem :: COUSIN2:43
for I being non empty closed_interval Subset of REAL
for f being PartFunc of I,REAL st f is lower_integrable holds
ex r being Real st
for D being Division of I holds lower_sum (f,D) < r
proof end;

theorem Th38: :: COUSIN2:44
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL
for D, D1 being Division of I st D . 1 = lower_bound I & D1 = D /^ 1 holds
( upper_sum (f,D1) = upper_sum (f,D) & lower_sum (f,D1) = lower_sum (f,D) )
proof end;

theorem Th39: :: COUSIN2:45
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being bounded integrable Function of I,REAL
for i being Nat st i in dom TD holds
( (lower_volume (f,(division_of TD))) . i <= (tagged_volume (f,TD)) . i & (tagged_volume (f,TD)) . i <= (upper_volume (f,(division_of TD))) . i )
proof end;

theorem Th40: :: COUSIN2:46
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being bounded integrable Function of I,REAL holds
( Sum (lower_volume (f,(division_of TD))) <= Sum (tagged_volume (f,TD)) & Sum (tagged_volume (f,TD)) <= Sum (upper_volume (f,(division_of TD))) )
proof end;

theorem Th41: :: COUSIN2:47
for I being non empty closed_interval Subset of REAL
for f being bounded integrable Function of I,REAL
for epsilon being Real st not I is trivial & 0 < epsilon holds
ex D being Division of I st
( D . 1 <> lower_bound I & upper_sum (f,D) < (integral f) + (epsilon / 2) & (integral f) - (epsilon / 2) < lower_sum (f,D) & (upper_sum (f,D)) - (lower_sum (f,D)) < epsilon )
proof end;

theorem :: COUSIN2:48
for I being non empty closed_interval Subset of REAL
for r being Real
for jauge being positive-yielding Function of I,REAL st jauge = r (#) (chi (I,I)) holds
0 < r
proof end;

theorem Th42: :: COUSIN2:49
for I being non empty closed_interval Subset of REAL
for r being Real
for jauge being positive-yielding Function of I,REAL
for D being tagged_division of I st jauge = r (#) (chi (I,I)) & D is jauge -fine holds
delta (division_of D) <= r
proof end;

theorem Th43: :: COUSIN2:50
for I being non empty closed_interval Subset of REAL
for D being Division of I
for fc being Function of I,REAL ex i being Nat st
( i in dom D & min (rng (upper_volume (fc,D))) = (upper_volume (fc,D)) . i )
proof end;

theorem Th44: :: COUSIN2:51
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for jauge being positive-yielding Function of I,REAL
for r1, r2, s being Real
for D1 being Division of I
for fc, f being Function of I,REAL
for epsilon being Real st fc = chi (I,I) & r1 = min (rng (upper_volume (fc,D1))) & r2 = epsilon / ((2 * (len D1)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|) & 0 < r1 & 0 < r2 & s = (min (r1,r2)) / 2 & jauge = s (#) fc & TD is jauge -fine holds
( delta (division_of TD) < min (rng (upper_volume (fc,D1))) & delta (division_of TD) < epsilon / ((2 * (len D1)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|) )
proof end;

theorem Th45: :: COUSIN2:52
for r being Real
for p being FinSequence of REAL st ( for i being Nat st i in dom p holds
r <= p . i ) & ex i0 being Nat st
( i0 in dom p & p . i0 = r ) holds
r = inf (rng p)
proof end;

theorem Th46: :: COUSIN2:53
for I being non empty closed_interval Subset of REAL
for D being Division of I
for fc being Function of I,REAL st fc = chi (I,I) holds
( 0 <= min (rng (upper_volume (fc,D))) & ( 0 = min (rng (upper_volume (fc,D))) implies divset (D,1) = [.(D . 1),(D . 1).] ) & ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) ) )
proof end;

theorem Th47: :: COUSIN2:54
for I being non empty closed_interval Subset of REAL
for D being Division of I st divset (D,1) = [.(D . 1),(D . 1).] holds
D . 1 = lower_bound I
proof end;

theorem Th48: :: COUSIN2:55
for I being non empty closed_interval Subset of REAL
for f being bounded integrable Function of I,REAL holds
( f is HK-integrable & HK-integral f = integral f )
proof end;

registration
let I be non empty closed_interval Subset of REAL;
cluster Function-like V55(I, REAL ) bounded integrable -> HK-integrable for Element of bool [:I,REAL:];
coherence
for b1 being Function of I,REAL st b1 is bounded & b1 is integrable holds
b1 is HK-integrable by Th48;
end;