let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st I is_closed_on s holds
insloc 0 in dom I
let s be State of SCM+FSA ; :: thesis: ( I is_closed_on s implies insloc 0 in dom I )
assume A1: I is_closed_on s ; :: thesis: insloc 0 in dom I
A2: IC SCM+FSA in dom (I +* (Start-At (insloc 0 ))) by SF_MASTR:65;
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) = (s +* (I +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by AMI_1:13
.= (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A2, FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ;
hence insloc 0 in dom I by A1, SCMFSA7B:def 7; :: thesis: verum