let k, x, n be Nat; :: thesis: ( n >= 1 & k >= 3 & x is_represented_by n + 1,k implies DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),(n + 1) = SDSub_Add_Carry (DigA (DecSD x,n,k),n),k )
assume that
A1: n >= 1 and
A2: k >= 3 ; :: thesis: ( not x is_represented_by n + 1,k or DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),(n + 1) = SDSub_Add_Carry (DigA (DecSD x,n,k),n),k )
set xn = x mod ((Radix k) |^ n);
A3: n + 1 in Seg (n + 1) by FINSEQ_1:5;
then DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),(n + 1) = SD2SDSubDigitS (DecSD (x mod ((Radix k) |^ n)),n,k),(n + 1),k by RADIX_3:def 8
.= SD2SDSubDigit (DecSD (x mod ((Radix k) |^ n)),n,k),(n + 1),k by A2, A3, RADIX_3:def 7, XXREAL_0:2
.= SDSub_Add_Carry (DigA (DecSD (x mod ((Radix k) |^ n)),n,k),((n + 1) -' 1)),k by RADIX_3:def 6
.= SDSub_Add_Carry (DigA (DecSD (x mod ((Radix k) |^ n)),n,k),(n + 0 )),k by NAT_D:34
.= SDSub_Add_Carry (DigA (DecSD x,n,k),n),k by A1, Lm3 ;
hence ( not x is_represented_by n + 1,k or DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),(n + 1) = SDSub_Add_Carry (DigA (DecSD x,n,k),n),k ) ; :: thesis: verum