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