let n, k be Nat; :: thesis: for x being Tuple of n,NAT
for y being Tuple of n,(k -SD ) st x = y holds
DigitSD2 x,k = DigitSD y
let x be Tuple of n,NAT ; :: thesis: for y being Tuple of n,(k -SD ) st x = y holds
DigitSD2 x,k = DigitSD y
let y be Tuple of n,(k -SD ); :: thesis: ( x = y implies DigitSD2 x,k = DigitSD y )
assume A1: x = y ; :: thesis: DigitSD2 x,k = DigitSD y

A2: now

let i be Element of NAT ; :: thesis: ( i in Seg n implies x . i = DigB y,i )
assume i in Seg n ; :: thesis: x . i = DigB y,i
then x . i = DigA y,i by A1, RADIX_1:def 3
.= DigB y,i by RADIX_1:def 4 ;
hence x . i = DigB y,i ; :: thesis: verum

end;

A3: ( len (DigitSD2 x,k) = n & len (DigitSD y) = n ) by FINSEQ_1:def 18;
then X: dom (DigitSD2 x,k) = Seg n by FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom (DigitSD2 x,k) implies (DigitSD2 x,k) . j = (DigitSD y) . j )
assume A4: j in dom (DigitSD2 x,k) ; :: thesis: (DigitSD2 x,k) . j = (DigitSD y) . j
then A5: ( j in dom (DigitSD2 x,k) & j in dom (DigitSD y) ) by A3, X, FINSEQ_1:def 3;
then (DigitSD2 x,k) . j = (DigitSD2 x,k) /. j by PARTFUN1:def 8
.= SubDigit2 x,j,k by A4, Def2, X
.= ((Radix k) |^ (j -' 1)) * (DigB y,j) by A2, A4, X
.= SubDigit y,j,k by RADIX_1:def 5
.= (DigitSD y) /. j by A4, X, RADIX_1:def 6
.= (DigitSD y) . j by A5, PARTFUN1:def 8 ;
hence (DigitSD2 x,k) . j = (DigitSD y) . j ; :: thesis: verum

end;

hence DigitSD2 x,k = DigitSD y by A3, FINSEQ_2:10; :: thesis: verum