:: deftheorem Def12 defines mindex DICKSON:def 12 :
for R being non empty 1-sorted
for f being sequence of R
for b being set
for m being Element of NAT st ex j being Element of NAT st
( m < j & f . j = b ) holds
for b₅ being Element of NAT holds
( b₅ = f mindex (b,m) iff ( f . b₅ = b & m < b₅ & ( for i being Element of NAT st m < i & f . i = b holds
b₅ <= i ) ) );