theorem Th29: :: SCMFSA_X:31

for I being really-closed MacroInstruction of SCM+FSA
for a being Int-Location
for k being Nat st k <= card I holds
(a =0_goto k) ";" I is really-closed