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 )
A1: len (DigitSD y) = n by FINSEQ_1:def 18;
A2: len (DigitSD2 x,k) = n by FINSEQ_1:def 18;
then A3: dom (DigitSD2 x,k) = Seg n by FINSEQ_1:def 3;
assume A4: x = y ; :: thesis: DigitSD2 x,k = DigitSD y

A5: 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 A4, RADIX_1:def 3
.= DigB y,i by RADIX_1:def 4 ;
hence x . i = DigB y,i ; :: thesis: verum

end;

now

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

end;

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