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