let k1, k2 be Tuple of n, NAT ; ( ( 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)
; k1 = k2
A6:
len k1 = n
by CARD_1:def 7;
then A7:
dom k1 = Seg n
by FINSEQ_1:def 3;
len k2 = n
by CARD_1:def 7;
hence
k1 = k2
by A6, A8, FINSEQ_2:9; verum