theorem Th18: :: SCMBSORT:28

for I, J being Program of
for i being Instruction of SCM+FSA holds ((I ";" i) ";" J) . ((card I) + 1) = goto ((card I) + 2)