theorem Th24: :: RADIX_1:25

for k, m, n being Nat st k >= 2 & m is_represented_by 1,k & n is_represented_by 1,k holds
SDDec ((DecSD (m,1,k)) '+' (DecSD (n,1,k))) = SD_Add_Data ((m + n),k)