theorem :: SCMFSA8B:32

for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA holds DataPart (Result ((P +* I),(Initialized s))) = DataPart (IExec (I,P,s)) by SCMFSA6B:def 1;