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

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