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 SCM+FSA holds DataPart (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = DataPart (IExec (I,P,s))
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds DataPart (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = DataPart (IExec (I,P,s))
let I be Program of SCM+FSA; :: thesis: DataPart (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = DataPart (IExec (I,P,s))
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set P1 = P +* I;
A1: IExec (I,P,s) = (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) by SCMFSA6B:def 1;

A2: now

let f be FinSeq-Location ; :: thesis: (IExec (I,P,s)) . f = (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . f
( f in dom (ProgramPart s) implies f is Element of NAT ) by COMPOS_1:34;
hence (IExec (I,P,s)) . f = (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . f by A1, FUNCT_4:12, SCMFSA_2:85; :: thesis: verum

end;

now

let b be Int-Location ; :: thesis: (IExec (I,P,s)) . b = (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . b
( b in dom (ProgramPart s) implies b is Element of NAT ) by COMPOS_1:34;
hence (IExec (I,P,s)) . b = (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . b by A1, FUNCT_4:12, SCMFSA_2:84; :: thesis: verum

end;

hence DataPart (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = DataPart (IExec (I,P,s)) by A2, SCMFSA6A:38; :: thesis: verum