theorem :: SCMFSA6A:19

for i, j being Instruction of SCM+FSA holds i ";" j = (Macro i) ";" j ;