:: deftheorem defDp1 defines Dp1 DUALSP05:def 2 :
for A being non empty closed_interval Subset of REAL
for D being Division of A
for m being Function of A,(BoundedFunctions A)
for i being Nat st i in Seg ((len D) + 1) holds
( ( i = 1 implies Dp1 (m,D,i) = m . (lower_bound A) ) & ( not i = 1 implies Dp1 (m,D,i) = m . (D . (i - 1)) ) );