let I be InitHalting Program of SCM+FSA ; :: thesis: insloc 0 in dom I
not dom I is empty by Th10;
then consider x being set such that
A1: x in dom I by XBOOLE_0:def 1;
dom I c= NAT by RELAT_1:def 18;
then reconsider x = x as Instruction-Location of SCM+FSA by A1, AMI_1:def 4;
reconsider n = x as Element of NAT by ORDINAL1:def 13;

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

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

hence insloc 0 in dom I by A1; :: thesis: verum

end;

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

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

end;

end;