theorem :: SCMFSA_M:19

for s being State of SCM+FSA st s . (intloc 0) = 1 holds
DataPart (Initialized s) = DataPart s