:: deftheorem defines lower_sum INTEGRA2:def 3 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for T being DivSequence of A
for b₄ being Real_Sequence holds
( b₄ = lower_sum (f,T) iff for i being Nat holds b₄ . i = lower_sum (f,(T . i)) );