theorem Th30: :: SCMPDS_7:32

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