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:96;
thus Initialized s = Initialize s by A2, FUNCT_4:14; :: thesis: verum