let I be Program of SCM+FSA; :: thesis: NPP (Initialized I) = Initialize ((intloc 0) .--> 1)
thus NPP (Initialized I) = NPP (Initialize ((intloc 0) .--> 1)) by COMPOS_1:224
.= Initialize (NPP ((intloc 0) .--> 1)) by COMPOS_1:207
.= Initialize ((intloc 0) .--> 1) by LmB ; :: thesis: verum