let k, m, n be Nat; :: thesis: ( m is_represented_by 1,k & n is_represented_by 1,k implies SD_Add_Carry ((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))) = SD_Add_Carry (m + n) )
assume that
A1: m is_represented_by 1,k and
A2: n is_represented_by 1,k ; :: thesis: SD_Add_Carry ((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))) = SD_Add_Carry (m + n)
SD_Add_Carry ((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))) = SD_Add_Carry (m + (DigA ((DecSD (n,1,k)),1))) by A1, Th20
.= SD_Add_Carry (m + n) by A2, Th20 ;
hence SD_Add_Carry ((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))) = SD_Add_Carry (m + n) ; :: thesis: verum