let m, k be Nat; ( 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
; 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
; verum