let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being Program of {INT,(INT *)}
for f being FinSeq-Location holds (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . f = (IExec (I,p,s)) . f
let s be State of SCM+FSA; :: thesis: for I being Program of {INT,(INT *)}
for f being FinSeq-Location holds (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . f = (IExec (I,p,s)) . f
let I be Program of {INT,(INT *)}; :: thesis: for f being FinSeq-Location holds (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . f = (IExec (I,p,s)) . f
let f be FinSeq-Location ; :: thesis: (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . f = (IExec (I,p,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 ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . f = (DataPart (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))) . f by FUNCT_1:72, SCMFSA_2:127
.= (DataPart (IExec (I,p,s))) . f by SCMFSA8B:35
.= (IExec (I,p,s)) . f by A1, FUNCT_1:72, SCMFSA_2:127 ;
:: thesis: verum