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