let k be Nat; :: thesis: 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 ; :: thesis: 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 ; :: thesis: verum