let k, m be Nat; ( m is_represented_by 1,k implies DigA ((DecSD (m,1,k)),1) = m )
assume
m is_represented_by 1,k
; DigA ((DecSD (m,1,k)),1) = m
then A1:
m < (Radix k) |^ 1
;
1 in Seg 1
by FINSEQ_1:1;
hence DigA ((DecSD (m,1,k)),1) =
DigitDC (m,1,k)
by Def9
.=
(m mod ((Radix k) |^ 1)) div ((Radix k) |^ 0)
by XREAL_1:232
.=
(m mod ((Radix k) |^ 1)) div 1
by NEWTON:4
.=
m mod ((Radix k) |^ 1)
by NAT_2:4
.=
m
by A1, NAT_D:24
;
verum