let k be Nat; for x being Tuple of 1,k -SD holds SDDec x = DigA (x,1)
1 - 1 = 0
;
then A1:
1 -' 1 = 0
by XREAL_0:def 2;
let x be Tuple of 1,k -SD ; SDDec x = DigA (x,1)
A2:
1 in Seg 1
by FINSEQ_1:2, TARSKI:def 1;
then A3:
(DigitSD x) /. 1 = SubDigit (x,1,k)
by RADIX_1:def 6;
A4:
len (DigitSD x) = 1
by CARD_1:def 7;
then
1 in dom (DigitSD x)
by A2, FINSEQ_1:def 3;
then A5:
(DigitSD x) . 1 = SubDigit (x,1,k)
by A3, PARTFUN1:def 6;
thus SDDec x =
Sum (DigitSD x)
by RADIX_1:def 7
.=
Sum <*(SubDigit (x,1,k))*>
by A4, A5, FINSEQ_1:40
.=
SubDigit (x,1,k)
by RVSUM_1:73
.=
((Radix k) |^ 0) * (DigB (x,1))
by A1, RADIX_1:def 5
.=
1 * (DigB (x,1))
by NEWTON:4
.=
DigA (x,1)
by RADIX_1:def 4
; verum