let s be State of SCM+FSA; :: thesis: for I being Program of {INT,(INT *)}
for f being FinSeq-Location holds (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) . f = (IExec (I,s)) . f
let I be Program of {INT,(INT *)}; :: 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