theorem :: SCMFSA6A:30

for i, k being Instruction of SCM+FSA
for J being Program of holds (i ";" J) ";" k = i ";" (J ";" k) by Th15;