let I be Program of SCM+FSA; :: thesis: ( I is keeping_0 implies I is keepInt0_1 )
assume A40: I is keeping_0 ; :: thesis: I is keepInt0_1

now

let s be State of SCM+FSA; :: thesis: ( Initialized I c= s implies for k being Element of NAT holds (Comput ((ProgramPart s),s,k)) . (intloc 0) = 1 )
assume A41: Initialized I c= s ; :: thesis: for k being Element of NAT holds (Comput ((ProgramPart s),s,k)) . (intloc 0) = 1
I +* (Start-At (0,SCM+FSA)) c= Initialized I by SCMFSA8C:19;
then A42: I +* (Start-At (0,SCM+FSA)) c= s by A41, XBOOLE_1:1;
s . (intloc 0) = 1 by A41, Th7;
hence for k being Element of NAT holds (Comput ((ProgramPart s),s,k)) . (intloc 0) = 1 by A40, A42, SCMFSA6B:def 4; :: thesis: verum

end;

hence I is keepInt0_1 by Def3; :: thesis: verum