theorem :: SCMPDS_6:106

for a being Int_position
for k1 being Integer
for I being Program of holds 0 in dom (if<0 (a,k1,I))