let m, k 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:21 ; :: thesis: verum