theorem Th4: :: SCMFSA6C:5

for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for i being sequential Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)