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

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