theorem Th40: :: SCMPDS_7:42

for a being Int_position
for i being Integer
for n, m being Nat
for I being Program of holds
( m < (card I) + 3 iff m in dom (for-down (a,i,n,I)) )