let k, m be Nat; :: thesis: ( 2 <= k & m is_represented_by 1,k implies DigA_SDSub (SD2SDSub (DecSD m,1,k)),(1 + 1) = SDSub_Add_Carry m,k )
assume A1: ( 2 <= k & m is_represented_by 1,k ) ; :: thesis: DigA_SDSub (SD2SDSub (DecSD m,1,k)),(1 + 1) = SDSub_Add_Carry m,k
hence DigA_SDSub (SD2SDSub (DecSD m,1,k)),(1 + 1) = SDSub_Add_Carry (DigA (DecSD m,1,k),1),k by Th3
.= SDSub_Add_Carry m,k by A1, RADIX_1:24 ;
:: thesis: verum