let s be State of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 implies Initialize s = s +* (Initialize ((intloc 0) .--> 1)) )
A1: intloc 0 in dom s by SCMFSA_2:66;
assume s . (intloc 0) = 1 ; :: thesis: Initialize s = s +* (Initialize ((intloc 0) .--> 1))
then A2: s = s +* ((intloc 0) .--> 1) by A1, FUNCT_7:111;
thus s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by SCMFSA8A:13
.= Initialize (Initialize s) by A2, FUNCT_4:15
.= Initialize s by FUNCT_4:99 ; :: thesis: verum