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