theorem Th9: :: SCPINVAR:9

for a being Int_position
for i being Integer
for m being Element of NAT
for I being Program of SCMPDS holds
( m < (card I) + 3 iff m in dom (while<>0 (a,i,I)) )