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 State of SCM+FSA; :: according to SCMFSA6B:def 4 :: thesis: ( not Start-At (0,SCM+FSA) c= s or 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) ) )
assume Start-At (0,SCM+FSA) c= s ; :: 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) )
then A3: Initialize s = s by FUNCT_4:103, FUNCT_4:104;
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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)
P +* I = P by A4, FUNCT_4:103, FUNCT_4:104;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A2, A3, Th27, A1, Th24; :: thesis: verum