theorem Th39: :: SCMPDS_7:41

for a being Int_position
for i being Integer
for n being Nat
for I being Program of holds card (for-down (a,i,n,I)) = (card I) + 3