let k1, k2 be Tuple of n,INT ; :: thesis: ( ( for i being Nat st i in Seg n holds
k1 /. i = SubDigit x,i,k ) & ( for i being Nat st i in Seg n holds
k2 /. i = SubDigit x,i,k ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg n holds
k1 /. i = SubDigit x,i,k and
A6: for i being Nat st i in Seg n holds
k2 /. i = SubDigit x,i,k ; :: thesis: k1 = k2
A7: ( len k1 = n & len k2 = n ) by FINSEQ_1:def 18;
X: dom k1 = Seg n by A7, FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A8: j in dom k1 ; :: thesis: k1 . j = k2 . j
then A9: ( j in dom k1 & j in dom k2 ) by A7, X, FINSEQ_1:def 3;
then k1 . j = k1 /. j by PARTFUN1:def 8
.= SubDigit x,j,k by A5, A8, X
.= k2 /. j by A6, A8, X
.= k2 . j by A9, PARTFUN1:def 8 ;
hence k1 . j = k2 . j ; :: thesis: verum

end;

hence k1 = k2 by A7, FINSEQ_2:10; :: thesis: verum