let k1, k2 be Tuple of n, NAT ; ( ( 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)
; 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 for j being Nat st j in dom k1 holds
k1 . j = k2 . jlet j be
Nat;
( j in dom k1 implies k1 . j = k2 . j )assume A10:
j in dom k1
;
k1 . j = k2 . jthen 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;
verum end;
hence
k1 = k2
by A7, A9, FINSEQ_2:9; verum