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 that
A1: 2 <= k and
A2: m is_represented_by 1,k ; :: thesis: DigA_SDSub (SD2SDSub (DecSD m,1,k)),(1 + 1) = SDSub_Add_Carry m,k
thus DigA_SDSub (SD2SDSub (DecSD m,1,k)),(1 + 1) = SDSub_Add_Carry (DigA (DecSD m,1,k),1),k by A1, Th3
.= SDSub_Add_Carry m,k by A2, RADIX_1:24 ; :: thesis: verum