theorem Th12: :: RADIX_5:12

for n being Nat st n >= 1 holds
for k being Nat
for tx, ty being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (tx,i) = DigA (ty,i) ) holds
SDDec tx = SDDec ty