let k, m 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:5;
A4: 1 in Seg (1 + 1) by FINSEQ_1:3;
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:234
.= (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:24
.= (SDSub_Add_Data m,k) + 0 by RADIX_3:17
.= m - ((SDSub_Add_Carry m,k) * (Radix k)) by RADIX_3:def 4 ;
:: thesis: verum