theorem :: SCMFSA_X:33
for I, J, K being MacroInstruction of SCM+FSA holds (I ";" J) ';' K = I ";" (J ';' K) by COMPOS_1:29;