for f being FinSeq-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for i being sequential keeping_0 Instruction of SCM+FSA
for j being sequential Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . f = (Exec (j,(Exec (i,(Initialized s))))) . f