let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA holds (s +* I) +* (Start-At (insloc 0 )) = (s +* (Start-At (insloc 0 ))) +* I
let s be State of SCM+FSA ; :: thesis: (s +* I) +* (Start-At (insloc 0 )) = (s +* (Start-At (insloc 0 ))) +* I
A1: dom I misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
then I +* (Start-At (insloc 0 )) = I \/ (Start-At (insloc 0 )) by FUNCT_4:32
.= (Start-At (insloc 0 )) +* I by A1, FUNCT_4:32 ;
hence (s +* I) +* (Start-At (insloc 0 )) = s +* ((Start-At (insloc 0 )) +* I) by FUNCT_4:15
.= (s +* (Start-At (insloc 0 ))) +* I by FUNCT_4:15 ;
:: thesis: verum