let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st s . (intloc 0 ) = 1 & IC s = insloc 0 holds
s +* I = s +* (Initialized I)
let I be Program of SCM+FSA ; :: thesis: ( s . (intloc 0 ) = 1 & IC s = insloc 0 implies s +* I = s +* (Initialized I) )
assume A1: ( s . (intloc 0 ) = 1 & IC s = insloc 0 ) ; :: thesis: s +* I = s +* (Initialized I)
A2: IC SCM+FSA in dom s by AMI_1:94;
thus s +* (Initialized I) = s +* (I +* (Start-At (insloc 0 ))) by A1, SCMFSA8C:18
.= (s +* I) +* (Start-At (insloc 0 )) by FUNCT_4:15
.= (s +* ((IC SCM+FSA ) .--> (insloc 0 ))) +* I by SCMFSA6B:14
.= s +* I by A1, A2, FUNCT_7:111 ; :: thesis: verum