let k, m, n be Nat; :: thesis: ( m is_represented_by n + 1,k implies DigA ((DecSD (m,(n + 1),k)),(n + 1)) = m div ((Radix k) |^ n) )
assume m is_represented_by n + 1,k ; :: thesis: DigA ((DecSD (m,(n + 1),k)),(n + 1)) = m div ((Radix k) |^ n)
then A1: m < (Radix k) |^ (n + 1) ;
n + 1 in Seg (n + 1) by FINSEQ_1:3;
then DigA ((DecSD (m,(n + 1),k)),(n + 1)) = DigitDC (m,(n + 1),k) by Def9
.= m div ((Radix k) |^ ((n + 1) -' 1)) by A1, NAT_D:24
.= m div ((Radix k) |^ n) by NAT_D:34 ;
hence DigA ((DecSD (m,(n + 1),k)),(n + 1)) = m div ((Radix k) |^ n) ; :: thesis: verum