let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA
for f being FinSeq-Location holds (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) . f = (IExec I,s) . f
let I be Program of SCM+FSA ; :: thesis: for f being FinSeq-Location holds (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) . f = (IExec I,s) . f
let f be FinSeq-Location ; :: thesis: (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) . f = (IExec I,s) . f
set D = Int-Locations \/ FinSeq-Locations ;
f in FinSeq-Locations by SCMFSA_2:10;
then A1: f in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
hence (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) . f = (DataPart (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) . f by FUNCT_1:72, SCMFSA_2:127
.= (DataPart (IExec I,s)) . f by SCMFSA8B:35
.= (IExec I,s) . f by A1, FUNCT_1:72, SCMFSA_2:127 ;
:: thesis: verum