for k being Nat holds 0 in k -SD_Sub