let k be Nat; for tx being Tuple of 1,k -SD holds SDDec tx = DigA (tx,1)
let tx be Tuple of 1,k -SD ; 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)
; verum