for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of
for f being FinSeq-Location holds (Result ((p +* I),(Initialized s))) . f = (IExec (I,p,s)) . f