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 CARD_1:def 7;
A2: len (DigitSD2 (x,k)) = n by CARD_1:def 7;
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 :: thesis: for i being Element of NAT st i in Seg n holds
x . i = DigB (y,i)

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 :: thesis: for j being Nat st j in dom (DigitSD2 (x,k)) holds
(DigitSD2 (x,k)) . j = (DigitSD y) . j

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 6
.= 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 6 ;
hence (DigitSD2 (x,k)) . j = (DigitSD y) . j ; :: thesis: verum

end;

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