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