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