let m, n, k 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) by Def12;
n + 1 in Seg (n + 1) by FINSEQ_1:5;
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