let s be State of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 implies DataPart (Initialized s) = DataPart s )
assume A1: s . (intloc 0) = 1 ; :: thesis: DataPart (Initialized s) = DataPart s
A2: intloc 0 in dom s by SCMFSA_2:42;
Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:14;
then Initialized s = Initialize s by A1, A2, FUNCT_7:96;
hence DataPart (Initialized s) = DataPart s by MEMSTR_0:79; :: thesis: verum