let k1, k2 be Tuple of n, NAT ; :: thesis: ( ( for i being Nat st i in Seg n holds

k1 /. i = SubDigit2 (x,i,k) ) & ( for i being Nat st i in Seg n holds

k2 /. i = SubDigit2 (x,i,k) ) implies k1 = k2 )

assume that

A5: for i being Nat st i in Seg n holds

k1 /. i = SubDigit2 (x,i,k) and

A6: for i being Nat st i in Seg n holds

k2 /. i = SubDigit2 (x,i,k) ; :: thesis: k1 = k2

A7: len k1 = n by CARD_1:def 7;

then A8: dom k1 = Seg n by FINSEQ_1:def 3;

A9: len k2 = n by CARD_1:def 7;

k1 /. i = SubDigit2 (x,i,k) ) & ( for i being Nat st i in Seg n holds

k2 /. i = SubDigit2 (x,i,k) ) implies k1 = k2 )

assume that

A5: for i being Nat st i in Seg n holds

k1 /. i = SubDigit2 (x,i,k) and

A6: for i being Nat st i in Seg n holds

k2 /. i = SubDigit2 (x,i,k) ; :: thesis: k1 = k2

A7: len k1 = n by CARD_1:def 7;

then A8: dom k1 = Seg n by FINSEQ_1:def 3;

A9: len k2 = n by CARD_1:def 7;

now :: thesis: for j being Nat st j in dom k1 holds

k1 . j = k2 . j

hence
k1 = k2
by A7, A9, FINSEQ_2:9; :: thesis: verumk1 . 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 A11: j in dom k2 by A9, A8, FINSEQ_1:def 3;

k1 . j = k1 /. j by A10, PARTFUN1:def 6

.= SubDigit2 (x,j,k) by A5, A8, A10

.= k2 /. j by A6, A8, A10 ;

hence k1 . j = k2 . j by A11, PARTFUN1:def 6; :: thesis: verum

end;assume A10: j in dom k1 ; :: thesis: k1 . j = k2 . j

then A11: j in dom k2 by A9, A8, FINSEQ_1:def 3;

k1 . j = k1 /. j by A10, PARTFUN1:def 6

.= SubDigit2 (x,j,k) by A5, A8, A10

.= k2 /. j by A6, A8, A10 ;

hence k1 . j = k2 . j by A11, PARTFUN1:def 6; :: thesis: verum