theorem :: SCMFSA6A:31

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