deffunc H₁( Nat) -> Element of k -SD = FSDMinDigit (m,k,$1);
consider z being FinSequence of k -SD such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H₁(j) from FINSEQ_2:sch 1();
A3: dom z = Seg n by A1, FINSEQ_1:def 3;
z is Element of n -tuples_on (k -SD) by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of n,k -SD ;
take z ; :: thesis: for i being Nat st i in Seg n holds
DigA (z,i) = FSDMinDigit (m,k,i)
let i be Nat; :: thesis: ( i in Seg n implies DigA (z,i) = FSDMinDigit (m,k,i) )
assume A4: i in Seg n ; :: thesis: DigA (z,i) = FSDMinDigit (m,k,i)
then DigA (z,i) = z . i by RADIX_1:def 3;
hence DigA (z,i) = FSDMinDigit (m,k,i) by A2, A3, A4; :: thesis: verum