let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I is_closed_on s holds
insloc 0 in dom I
let I be Program 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
reconsider n = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) as Element of NAT by ORDINAL1:def 13;
A3: insloc n in dom I by A1, SCMFSA7B:def 7;

per cases ( n = 0 or 0 < n ) ;

suppose n = 0 ; :: thesis: insloc 0 in dom I

hence insloc 0 in dom I by A1, SCMFSA7B:def 7; :: thesis: verum

end;

suppose 0 < n ; :: thesis: insloc 0 in dom I

hence insloc 0 in dom I by A3, SCMNORM:def 1; :: thesis: verum

end;

end;