let m, k, 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, Th24
.= SD_Add_Carry (m + n) by A2, Th24 ;
hence SD_Add_Carry ((DigA (DecSD m,1,k),1) + (DigA (DecSD n,1,k),1)) = SD_Add_Carry (m + n) ; :: thesis: verum