:: deftheorem Def6 defines Fmin RADIX_5:def 6 :
for n, m, k being Nat
for b₄ being Tuple of n,k -SD holds
( b₄ = Fmin (n,m,k) iff for i being Nat st i in Seg n holds
DigA (b₄,i) = FminDigit (m,k,i) );