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