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:66;
Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:15;
then Initialized s = Initialize s by A1, A2, FUNCT_7:111;
hence DataPart (Initialized s) = DataPart s by SCMFSA8A:10; :: thesis: verum