deffunc H_{1}( 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_{1}(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:92;

then reconsider z = z as Tuple of n + 1,k -SD_Sub ;

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

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

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:92;

then reconsider z = z as Tuple of n + 1,k -SD_Sub ;

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