let I be Program of ; :: thesis: ( I is really-closed & I is good implies I is keeping_0 )
assume A1: ( I is really-closed & I is good ) ; :: thesis: I is keeping_0
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def 4 :: thesis: for b₁ being set holds
( not I c= b₁ or for b₂ being set holds (Comput (b₁,s,b₂)) . (intloc 0) = s . (intloc 0) )
A2: Initialize s = s by MEMSTR_0:44;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not I c= P or for b₁ being set holds (Comput (P,s,b₁)) . (intloc 0) = s . (intloc 0) )
assume A3: I c= P ; :: thesis: for b₁ being set holds (Comput (P,s,b₁)) . (intloc 0) = s . (intloc 0)
let k be Nat; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
P +* I = P by A3, FUNCT_4:98;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A1, A2, Th20; :: thesis: verum