let k, m, n 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 <= n by NAT_1:2;
then 0 + 1 <= n + 1 by XREAL_1:9;
then A2: n + 1 in Seg (n + 1) by FINSEQ_1:3;
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