deffunc H₁( Element of NAT ) -> FinSequence of INT = <*> INT ;
deffunc H₂( Element of NAT ) -> Element of K530() = 1;
deffunc H₃( Element of NAT ) -> Element of the Instructions of SCM+FSA = goto (insloc 0 );
let I be InitHalting Program of ; :: thesis: dom I <> {}
assume A1: dom I = {} ; :: thesis: contradiction
consider s being State of such that
A2: IC s = insloc 0 and
A3: for i being Element of NAT holds
( s . (insloc i) = H₃(i) & s . (intloc i) = H₂(i) & s . (fsloc i) = H₁(i) ) from SCMFSA6A:sch 1();
s . (insloc 0 ) = goto (insloc 0 ) by A3;
then s +* (IC s),(goto (IC s)) = s by A2, FUNCT_7:37;
then A4: not ProgramPart s halts_on s by SCMFSA6B:20;
A5: dom (Initialized I) = ((dom I) \/ {(intloc 0 )}) \/ {(IC SCM+FSA )} by SCMFSA6A:43
.= {(intloc 0 )} \/ {(IC SCM+FSA )} by A1 ;

A6: now

let x be set ; :: thesis: ( x in dom (Initialized I) implies (Initialized I) . b₁ = s . b₁ )
A7: dom (Initialized I) = {(intloc 0 ),(IC SCM+FSA )} by A5, ENUMSET1:41;
assume A8: x in dom (Initialized I) ; :: thesis: (Initialized I) . b₁ = s . b₁

per cases ( x = intloc 0 or x = IC SCM+FSA ) by A8, A7, TARSKI:def 2;

suppose A9: x = intloc 0 ; :: thesis: (Initialized I) . b₁ = s . b₁

hence (Initialized I) . x = 1 by SCMFSA6A:46
.= s . x by A3, A9 ;
:: thesis: verum

end;

suppose x = IC SCM+FSA ; :: thesis: (Initialized I) . b₁ = s . b₁

hence (Initialized I) . x = s . x by A2, SCMFSA6A:46; :: thesis: verum

end;

end;

end;

A10: intloc 0 in Int-Locations by SCMFSA_2:9;
A11: dom s = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by AMI_1:79, SCMFSA_2:8;
then dom s = ((FinSeq-Locations \/ {(IC SCM+FSA )}) \/ Int-Locations ) \/ NAT by XBOOLE_1:4
.= ((FinSeq-Locations \/ {(IC SCM+FSA )}) \/ NAT ) \/ Int-Locations by XBOOLE_1:4 ;
then intloc 0 in dom s by A10, XBOOLE_0:def 3;
then for x being set st x in {(intloc 0 )} holds
x in dom s by TARSKI:def 1;
then A12: {(intloc 0 )} c= dom s by TARSKI:def 3;
dom s = {(IC SCM+FSA )} \/ ((Int-Locations \/ FinSeq-Locations ) \/ NAT ) by A11, XBOOLE_1:4;
then {(IC SCM+FSA )} c= dom s by XBOOLE_1:7;
then dom (Initialized I) c= dom s by A12, A5, XBOOLE_1:8;
then Initialized I c= s by A6, GRFUNC_1:8;
hence contradiction by A4, AMI_1:def 26; :: thesis: verum