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)
reconsider w = DigA (tx,1) as Element of INT by INT_1:def 2;
A1: 1 in Seg 1 by FINSEQ_1:1;
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:232
.= 1 * (DigA (tx,1)) by NEWTON:4 ;
A3: len (DigitSD tx) = 1 by CARD_1:def 7;
then 1 in dom (DigitSD tx) by A1, FINSEQ_1:def 3;
then A4: (DigitSD tx) . 1 = DigA (tx,1) by A2, PARTFUN1:def 6;
SDDec tx = Sum (DigitSD tx) by RADIX_1:def 7
.= Sum <*w*> by A3, A4, FINSEQ_1:40
.= DigA (tx,1) by RVSUM_1:73 ;
hence SDDec tx = DigA (tx,1) ; :: thesis: verum