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