theorem :: SCMFSA6A:29

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