deffunc H₁( Nat) -> Element of k -SD = M0Digit 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 = H₁(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:110;
then reconsider z = z as Tuple of m + 2,k -SD by A1, FINSEQ_2:151;
take z ; :: thesis: for i being Nat st i in Seg (m + 2) holds
DigA z,i = M0Digit r,i
let i be Nat; :: thesis: ( i in Seg (m + 2) implies DigA z,i = M0Digit r,i )
assume A4: i in Seg (m + 2) ; :: thesis: DigA z,i = M0Digit r,i
hence DigA z,i = z . i by RADIX_1:def 3
.= M0Digit r,i by A2, A3, A4 ;
:: thesis: verum