let k1, k2 be Tuple of m + 2,k -SD ; :: thesis: ( ( for i being Nat st i in Seg (m + 2) holds
DigA (k1,i) = M0Digit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds
DigA (k2,i) = M0Digit (r,i) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg (m + 2) holds
DigA (k1,i) = M0Digit (r,i) and
A6: for i being Nat st i in Seg (m + 2) holds
DigA (k2,i) = M0Digit (r,i) ; :: thesis: k1 = k2
A7: len k1 = m + 2 by CARD_1:def 7;
then A8: dom k1 = Seg (m + 2) by FINSEQ_1:def 3;

A9: now :: thesis: for j being Nat st j in dom k1 holds
k1 . j = k2 . j

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 (k1,j) by A8, RADIX_1:def 3
.= M0Digit (r,j) by A5, A8, A10
.= DigA (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, RADIX_1:def 3 ;
hence k1 . j = k2 . j ; :: thesis: verum

end;

len k2 = m + 2 by CARD_1:def 7;
hence k1 = k2 by A7, A9, FINSEQ_2:9; :: thesis: verum