let k be Nat; :: thesis: for tx being Tuple of 1,(k -SD ) holds SDDec tx = DigA tx,1
let tx be Tuple of 1,(k -SD ); :: thesis: SDDec tx = DigA tx,1
A1: 1 in Seg 1 by FINSEQ_1:3;
then A2: (DigitSD tx) /. 1 = SubDigit tx,1,k by RADIX_1:def 6
.= ((Radix k) |^ (1 -' 1)) * (DigB tx,1) by RADIX_1:def 5
.= ((Radix k) |^ (1 -' 1)) * (DigA tx,1) by RADIX_1:def 4
.= ((Radix k) |^ 0 ) * (DigA tx,1) by XREAL_1:234
.= 1 * (DigA tx,1) by NEWTON:9 ;
A3: len (DigitSD tx) = 1 by FINSEQ_1:def 18;
then 1 in dom (DigitSD tx) by A1, FINSEQ_1:def 3;
then A4: (DigitSD tx) . 1 = DigA tx,1 by A2, PARTFUN1:def 8;
reconsider w = DigA tx,1 as Element of INT by INT_1:def 2;
SDDec tx = Sum (DigitSD tx) by RADIX_1:def 7
.= Sum <*w*> by A3, A4, FINSEQ_1:57
.= DigA tx,1 by RVSUM_1:103 ;
hence SDDec tx = DigA tx,1 ; :: thesis: verum