let n, m, k be Nat; :: thesis: ( 2 <= k implies DigA_SDSub ((SD2SDSub (DecSD (m,n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (m,n,k)),n)),k) )
assume A1: 2 <= k ; :: thesis: DigA_SDSub ((SD2SDSub (DecSD (m,n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (m,n,k)),n)),k)
0 + 1 <= n + 1 by XREAL_1:7;
then A2: n + 1 in Seg (n + 1) by FINSEQ_1:1;
hence DigA_SDSub ((SD2SDSub (DecSD (m,n,k))),(n + 1)) = SD2SDSubDigitS ((DecSD (m,n,k)),(n + 1),k) by RADIX_3:def 8
.= SD2SDSubDigit ((DecSD (m,n,k)),(n + 1),k) by A1, A2, RADIX_3:def 7
.= SDSub_Add_Carry ((DigA ((DecSD (m,n,k)),((n + 1) -' 1))),k) by RADIX_3:def 6
.= SDSub_Add_Carry ((DigA ((DecSD (m,n,k)),n)),k) by NAT_D:34 ;
:: thesis: verum