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