begin
Lm1:
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is upper_integrable & upper_integral f = 0 )
Lm2:
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is lower_integrable & lower_integral f = 0 )
begin
Lm3:
for A being non empty closed_interval Subset of REAL
for n being Element of NAT st n > 0 & vol A > 0 holds
ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )
Lm4:
for A being non empty closed_interval Subset of REAL st vol A > 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
Lm5:
for A being non empty closed_interval Subset of REAL st vol A = 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )