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 rho being Function of A,REAL ex s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st
( len s = len D & ( for i being Nat st i in dom s holds
s . i = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) ) )