:: deftheorem Def11 defines mindex DICKSON:def 11 :
for f being Function
for b being set st dom f = NAT & b in rng f holds
for b₃ being Element of NAT holds
( b₃ = f mindex b iff ( f . b₃ = b & ( for i being Element of NAT st f . i = b holds
b₃ <= i ) ) );