let s be State of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 & IC s = 0 implies Initialized s = s )
assume A1: s . (intloc 0) = 1 ; :: thesis: ( not IC s = 0 or Initialized s = s )
assume A2: IC s = 0 ; :: thesis: Initialized s = s
A3: IC in dom s by MEMSTR_0:2;
A4: intloc 0 in dom s by SCMFSA_2:42;
thus Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:14
.= s +* ((IC ) .--> 0) by A1, A4, FUNCT_7:96
.= s by A2, A3, FUNCT_7:96 ; :: thesis: verum