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_{1} being set holds

( not I c= b_{1} or for b_{2} being set holds (Comput (b_{1},s,b_{2})) . (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_{1} being set holds (Comput (P,s,b_{1})) . (intloc 0) = s . (intloc 0) )

assume A3: I c= P ; :: thesis: for b_{1} being set holds (Comput (P,s,b_{1})) . (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

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

( not I c= b

A2: Initialize s = s by MEMSTR_0:44;

let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not I c= P or for b

assume A3: I c= P ; :: thesis: for b

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