let s be State of SCM+FSA ; :: thesis: ( s . (intloc 0 ) = 1 implies DataPart (Initialize s) = DataPart s )
assume A1: s . (intloc 0 ) = 1 ; :: thesis: DataPart (Initialize s) = DataPart s
A2: ( intloc 0 in dom s & IC SCM+FSA in dom s ) by AMI_1:94, SCMFSA_2:66;
Initialize s = (s +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 )) by SCMFSA6C:def 3
.= s +* (Start-At (insloc 0 )) by A1, A2, FUNCT_7:111 ;
hence DataPart (Initialize s) = DataPart s by SCMFSA8A:10; :: thesis: verum