let p be Instruction-Sequence of SCM+FSA; :: thesis: 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
let s be State of SCM+FSA; :: thesis: for I being Program of
for f being FinSeq-Location holds (Result ((p +* I),(Initialized s))) . f = (IExec (I,p,s)) . f
let I be Program of ; :: thesis: for f being FinSeq-Location holds (Result ((p +* I),(Initialized s))) . f = (IExec (I,p,s)) . f
let f be FinSeq-Location ; :: thesis: (Result ((p +* I),(Initialized s))) . f = (IExec (I,p,s)) . f
set D = Int-Locations \/ FinSeq-Locations;
f in FinSeq-Locations by SCMFSA_2:def 5;
then A1: f in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
hence (Result ((p +* I),(Initialized s))) . f = (DataPart (Result ((p +* I),(Initialized s)))) . f by FUNCT_1:49, SCMFSA_2:100
.= (DataPart (IExec (I,p,s))) . f by SCMFSA8B:32
.= (IExec (I,p,s)) . f by A1, FUNCT_1:49, SCMFSA_2:100 ;
:: thesis: verum