let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s)
let I be Program of SCM+FSA; :: thesis: s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s)
thus s +* (Initialize ((intloc 0) .--> 1)) = s +* ((Initialize ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:99
.= Initialize (Initialized s) by FUNCT_4:15 ; :: thesis: verum