let k1, k2 be Tuple of n, NAT ; :: thesis: ( ( for i being Nat st i in Seg n holds
k1 . i = DigitDC2 (x,i,k) ) & ( for i being Nat st i in Seg n holds
k2 . i = DigitDC2 (x,i,k) ) implies k1 = k2 )
assume that
A4: for i being Nat st i in Seg n holds
k1 . i = DigitDC2 (x,i,k) and
A5: for i being Nat st i in Seg n holds
k2 . i = DigitDC2 (x,i,k) ; :: thesis: k1 = k2
A6: len k1 = n by CARD_1:def 7;
then A7: dom k1 = Seg n by FINSEQ_1:def 3;

A8: 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 A9: j in dom k1 ; :: thesis: k1 . j = k2 . j
then k1 . j = DigitDC2 (x,j,k) by A4, A7;
hence k1 . j = k2 . j by A5, A7, A9; :: thesis: verum

end;

len k2 = n by CARD_1:def 7;
hence k1 = k2 by A6, A8, FINSEQ_2:9; :: thesis: verum