let I be Program of SCM+FSA ; :: thesis: ( I is keeping_0 implies I is keepInt0_1 )
assume A44: 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 (Computation s,k) . (intloc 0 ) = 1 )
assume A45: Initialized I c= s ; :: thesis: for k being Element of NAT holds (Computation s,k) . (intloc 0 ) = 1
then A46: s . (intloc 0 ) = 1 by Th7;
I +* (Start-At (insloc 0 )) c= Initialized I by SCMFSA8C:19;
then I +* (Start-At (insloc 0 )) c= s by A45, XBOOLE_1:1;
hence for k being Element of NAT holds (Computation s,k) . (intloc 0 ) = 1 by A44, A46, SCMFSA6B:def 4; :: thesis: verum

end;

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