let m, k be Nat; :: thesis: ( 2 <= k & m is_represented_by 1,k implies DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = m - ((SDSub_Add_Carry (m,k)) * (Radix k)) )
assume that
A1: 2 <= k and
A2: m is_represented_by 1,k ; :: thesis: DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = m - ((SDSub_Add_Carry (m,k)) * (Radix k))
A3: 1 in Seg 1 by FINSEQ_1:3;
A4: 1 in Seg (1 + 1) by FINSEQ_1:1;
then DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = SD2SDSubDigitS ((DecSD (m,1,k)),1,k) by RADIX_3:def 8
.= SD2SDSubDigit ((DecSD (m,1,k)),1,k) by A1, A4, RADIX_3:def 7 ;
hence DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = (SDSub_Add_Data ((DigA ((DecSD (m,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,1,k)),(1 -' 1))),k)) by A3, RADIX_3:def 6
.= (SDSub_Add_Data ((DigA ((DecSD (m,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,1,k)),0)),k)) by XREAL_1:232
.= (SDSub_Add_Data ((DigA ((DecSD (m,1,k)),1)),k)) + (SDSub_Add_Carry (0,k)) by RADIX_1:def 3
.= (SDSub_Add_Data (m,k)) + (SDSub_Add_Carry (0,k)) by A2, RADIX_1:21
.= (SDSub_Add_Data (m,k)) + 0 by RADIX_3:16
.= m - ((SDSub_Add_Carry (m,k)) * (Radix k)) by RADIX_3:def 4 ;
:: thesis: verum