let s be State of SCM+FSA; :: thesis: for I being InitHalting keepInt0_1 Program of SCM+FSA holds (IExec (I,s)) . (intloc 0) = 1
let I be InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: (IExec (I,s)) . (intloc 0) = 1
not intloc 0 in NAT

proof

A1: intloc 0 in Int-Locations by SCMFSA_2:9;
assume intloc 0 in NAT ; :: thesis: contradiction
hence contradiction by A1, SCMFSA_2:13, XBOOLE_0:3; :: thesis: verum

end;

then A2: not intloc 0 in dom (s | NAT) by RELAT_1:86;
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by Th5, FUNCT_4:26;
then A3: ( Initialized I c= s +* (Initialized I) & ex n being Element of NAT st
( Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) = Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) & CurInstr ((ProgramPart (s +* (Initialized I))),(Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))) = halt SCM+FSA ) ) by EXTPRO_1:def 8, FUNCT_4:26;
thus (IExec (I,s)) . (intloc 0) = ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (s | NAT)) . (intloc 0) by SCMFSA6B:def 1
.= (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) . (intloc 0) by A2, FUNCT_4:12
.= 1 by A3, Def3 ; :: thesis: verum