let k1, k2 be Tuple of n + 1,k -SD_Sub ; :: thesis: ( ( for i being Nat st i in Seg (n + 1) holds
DigA_SDSub k1,i = SD2SDSubDigitS x,i,k ) & ( for i being Nat st i in Seg (n + 1) holds
DigA_SDSub k2,i = SD2SDSubDigitS x,i,k ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg (n + 1) holds
DigA_SDSub k1,i = SD2SDSubDigitS x,i,k and
A6: for i being Nat st i in Seg (n + 1) holds
DigA_SDSub k2,i = SD2SDSubDigitS x,i,k ; :: thesis: k1 = k2
A7: len k1 = n + 1 by FINSEQ_1:def 18;
then A8: dom k1 = Seg (n + 1) by FINSEQ_1:def 3;

A9: now

let j be Nat; :: thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; :: thesis: k1 . j = k2 . j
then k1 . j = DigA_SDSub k1,j by A8, Def5
.= SD2SDSubDigitS x,j,k by A5, A8, A10
.= DigA_SDSub k2,j by A6, A8, A10
.= k2 . j by A8, A10, Def5 ;
hence k1 . j = k2 . j ; :: thesis: verum

end;

len k2 = n + 1 by FINSEQ_1:def 18;
hence k1 = k2 by A7, A9, FINSEQ_2:10; :: thesis: verum