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 (insloc 0 ))) = s +* (Initialized I)
let I be Program of SCM+FSA ; :: thesis: ( s . (intloc 0 ) = 1 implies s +* (I +* (Start-At (insloc 0 ))) = s +* (Initialized I) )
assume A1: s . (intloc 0 ) = 1 ; :: thesis: s +* (I +* (Start-At (insloc 0 ))) = s +* (Initialized I)
intloc 0 in dom s by SCMFSA_2:66;
then A2: s = s +* ((intloc 0 ) .--> 1) by A1, FUNCT_7:111;
thus s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:13
.= ((Initialize s) +* I) +* (Start-At (insloc 0 )) by FUNCT_4:15
.= ((Initialize s) +* (Start-At (insloc 0 ))) +* I by SCMFSA6B:14
.= ((s +* (Start-At (insloc 0 ))) +* (Start-At (insloc 0 ))) +* I by A2, SCMFSA6C:def 3
.= (s +* ((Start-At (insloc 0 )) +* (Start-At (insloc 0 )))) +* I by FUNCT_4:15
.= (s +* I) +* (Start-At (insloc 0 )) by SCMFSA6B:14
.= s +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:15 ; :: thesis: verum