theorem :: SCMFSA6A:28

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