theorem :: SCMFSA6A:27

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