let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA
for a being Int-Location holds Result (s +* (Initialized I)), IExec I,s equal_outside NAT
let I be Program of SCM+FSA ; :: thesis: for a being Int-Location holds Result (s +* (Initialized I)), IExec I,s equal_outside NAT
let a be Int-Location ; :: thesis: Result (s +* (Initialized I)), IExec I,s equal_outside NAT
set s1 = s +* (Initialized I);
DataPart (Result (s +* (Initialized I))) = DataPart (IExec I,s) by Th35;
then A1: ( ( for a being Int-Location holds (Result (s +* (Initialized I))) . a = (IExec I,s) . a ) & ( for f being FinSeq-Location holds (Result (s +* (Initialized I))) . f = (IExec I,s) . f ) ) by SCMFSA6A:38;
IC (Result (s +* (Initialized I))) = IC (IExec I,s) by SCMFSA8A:7;
hence Result (s +* (Initialized I)), IExec I,s equal_outside NAT by A1, SCMFSA6A:28; :: thesis: verum