let k, x, n be Nat; :: thesis: ( n >= 1 implies DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n) = DigA ((DecSD (x,n,k)),n) )
set xn = x mod ((Radix k) |^ n);
assume n >= 1 ; :: thesis: DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n) = DigA ((DecSD (x,n,k)),n)
then n <> 0 ;
then A1: n in Seg n by FINSEQ_1:3;
then DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n) = DigitDC ((x mod ((Radix k) |^ n)),n,k) by RADIX_1:def 9
.= DigitDC (x,n,k) by EULER_2:5
.= DigA ((DecSD (x,n,k)),n) by A1, RADIX_1:def 9 ;
hence DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n) = DigA ((DecSD (x,n,k)),n) ; :: thesis: verum