theorem :: SCMFSA6A:20

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