:: deftheorem Def2 defines min_p RFINSEQ2:def 2 :
for f being real-valued FinSequence
for b₂ being Nat holds
( b₂ = min_p f iff ( ( len f = 0 implies b₂ = 0 ) & ( len f > 0 implies ( b₂ in dom f & ( for i being Nat st i in dom f holds
f . i >= f . b₂ ) & ( for j being Nat st j in dom f & f . j = f . b₂ holds
b₂ <= j ) ) ) ) );