theorem :: SCMFSA_M:13

for p being PartState of SCM+FSA holds Initialize ((intloc 0) .--> 1) c= Initialized p by FUNCT_4:25;