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