:: deftheorem Def2 defines delta INTEGRA3:def 2 :
for A being non empty closed_interval Subset of REAL
for T being DivSequence of A
for b₃ being Real_Sequence holds
( b₃ = delta T iff for i being Element of NAT holds b₃ . i = delta (T . i) );