deffunc H₁( Nat) -> Element of k -SD_Sub = SD2SDSubDigitS x,$1,k;
consider z being FinSequence of k -SD_Sub such that
A1: len z = n + 1 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 + 1) by A1, FINSEQ_1:def 3;
z is Element of (n + 1) -tuples_on (k -SD_Sub ) by A1, FINSEQ_2:110;
then reconsider z = z as Tuple of n + 1,k -SD_Sub by A1, FINSEQ_2:151;
take z ; :: thesis: for i being Nat st i in Seg (n + 1) holds
DigA_SDSub z,i = SD2SDSubDigitS x,i,k
let i be Nat; :: thesis: ( i in Seg (n + 1) implies DigA_SDSub z,i = SD2SDSubDigitS x,i,k )
assume A4: i in Seg (n + 1) ; :: thesis: DigA_SDSub z,i = SD2SDSubDigitS x,i,k
hence DigA_SDSub z,i = z . i by Def5
.= SD2SDSubDigitS x,i,k by A2, A3, A4 ;
:: thesis: verum