let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I)
let I be Program of SCM+FSA; :: thesis: s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I)
Initialized I = Initialize (I +* ((intloc 0) .--> 1)) by FUNCT_4:15;
then Start-At (0,SCM+FSA) c= Initialized I by FUNCT_4:26;
hence s +* (Initialize (Initialized I)) = s +* (Initialized I) by FUNCT_4:79
.= (Initialized s) +* (Initialize I) by SCMFSA8A:13 ;
:: thesis: verum