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:3;
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