theorem :: SCMFSA6A:26

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