:: deftheorem Def18 defines indx INTEGRA1:def 19 :
for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A
for i being Nat st D1 <= D2 holds
for b₅ being Element of NAT holds
( ( i in dom D1 implies ( b₅ = indx (D2,D1,i) iff ( b₅ in dom D2 & D1 . i = D2 . b₅ ) ) ) & ( not i in dom D1 implies ( b₅ = indx (D2,D1,i) iff b₅ = 0 ) ) );