let k1, k2 be Tuple of n,k -SD ; ( ( for i being Nat st i in Seg n holds
DigA (k1,i) = FminDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (k2,i) = FminDigit (m,k,i) ) implies k1 = k2 )
assume that
A5:
for i being Nat st i in Seg n holds
DigA (k1,i) = FminDigit (m,k,i)
and
A6:
for i being Nat st i in Seg n holds
DigA (k2,i) = FminDigit (m,k,i)
; k1 = k2
A7:
len k1 = n
by CARD_1:def 7;
then A8:
dom k1 = Seg n
by FINSEQ_1:def 3;
A9:
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 k1 . j =
DigA (
k1,
j)
by A8, RADIX_1:def 3
.=
FminDigit (
m,
k,
j)
by A5, A8, A10
.=
DigA (
k2,
j)
by A6, A8, A10
.=
k2 . j
by A8, A10, RADIX_1:def 3
;
hence
k1 . j = k2 . j
;
verum end;
len k2 = n
by CARD_1:def 7;
hence
k1 = k2
by A7, A9, FINSEQ_2:9; verum