for k being Nat holds SD_Add_Data (0,k) = 0 by Th17;