let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st s . (intloc 0 ) = 1 holds
s +* (I +* (Start-At 0 ,SCM+FSA )) = s +* (Initialized I)
let I be Program of SCM+FSA ; :: thesis: ( s . (intloc 0 ) = 1 implies s +* (I +* (Start-At 0 ,SCM+FSA )) = s +* (Initialized I) )
A1: intloc 0 in dom s by SCMFSA_2:66;
assume s . (intloc 0 ) = 1 ; :: thesis: s +* (I +* (Start-At 0 ,SCM+FSA )) = s +* (Initialized I)
then A2: s = s +* ((intloc 0 ) .--> 1) by A1, FUNCT_7:111;
thus s +* (Initialized I) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13
.= ((Initialized s) +* I) +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:15
.= ((Initialized s) +* (Start-At 0 ,SCM+FSA )) +* I by SCMFSA6B:14
.= ((s +* (Start-At 0 ,SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) +* I by A2, SCMFSA6A:def 4
.= (s +* ((Start-At 0 ,SCM+FSA ) +* (Start-At 0 ,SCM+FSA ))) +* I by FUNCT_4:15
.= (s +* I) +* (Start-At 0 ,SCM+FSA ) by SCMFSA6B:14
.= s +* (I +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:15 ; :: thesis: verum