:: deftheorem Def1 defines min MATRIXJ1:def 1 :
for f being FinSequence of NAT
for i being Nat st i in Seg (Sum f) holds
for b₃ being Element of NAT holds
( b₃ = min (f,i) iff ( i <= Sum (f | b₃) & b₃ in dom f & ( for j being Nat st i <= Sum (f | j) holds
b₃ <= j ) ) );