let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds s +* ((Initialized I) +* (Start-At (insloc 0 ))) = (Initialize s) +* (I +* (Start-At (insloc 0 )))
let I be Program of SCM+FSA ; :: thesis: s +* ((Initialized I) +* (Start-At (insloc 0 ))) = (Initialize s) +* (I +* (Start-At (insloc 0 )))
Start-At (insloc 0 ) c= Initialized I by SCMFSA6B:4;
hence s +* ((Initialized I) +* (Start-At (insloc 0 ))) = s +* (Initialized I) by FUNCT_4:79
.= (Initialize s) +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:13 ;
:: thesis: verum