theorem :: SCMPDS_6:55

for a being Int_position
for k1 being Integer
for I being Program of holds card (if<>0 (a,k1,I)) = (card I) + 2 by Lm8;