let I be Program of SCM+FSA; :: thesis: ( I is paraclosed & I is good implies I is keeping_0 )
assume A1: ( I is paraclosed & I is good ) ; :: thesis: I is keeping_0
then A2: not I destroys intloc 0 by Def5;
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 Element of NAT holds (Comput (b₁,s,b₂)) . (intloc 0) = s . (intloc 0) )
A3: Initialize s = s by MEMSTR_0:44;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not I c= P or for b₁ being Element of NAT holds (Comput (P,s,b₁)) . (intloc 0) = s . (intloc 0) )
assume A4: I c= P ; :: thesis: for b₁ being Element of NAT holds (Comput (P,s,b₁)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
XX: I is_closed_on s,P by A1, Th24;
P +* I = P by A4, FUNCT_4:98;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A2, A3, Th27, XX; :: thesis: verum