theorem :: SCMPDS_6:16

for a being Int_position
for k1, k2 being Integer holds (a,k1) <>0_goto k2 <> halt SCMPDS