:: deftheorem Def8 defines Fmax RADIX_5:def 8 :
for n, m, k being Nat
for b₄ being Tuple of n,k -SD holds
( b₄ = Fmax (n,m,k) iff for i being Nat st i in Seg n holds
DigA (b₄,i) = FmaxDigit (m,k,i) );