let I be InitHalting Program of SCM+FSA ; :: thesis: dom I <> {}
assume A1: dom I = {} ; :: thesis: contradiction
deffunc H₁( Element of NAT ) -> Element of the Instructions of SCM+FSA = goto (insloc 0 );
deffunc H₂( Element of NAT ) -> Element of K352() = 1;
deffunc H₃( Element of NAT ) -> FinSequence of INT = <*> INT ;
consider s being State of SCM+FSA 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();
A4: dom s = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by AMI_1:79, SCMFSA_2:8;
then A5: dom s = {(IC SCM+FSA )} \/ ((Int-Locations \/ FinSeq-Locations ) \/ NAT ) by XBOOLE_1:4;
A6: dom s = ((FinSeq-Locations \/ {(IC SCM+FSA )}) \/ Int-Locations ) \/ NAT by A4, XBOOLE_1:4
.= ((FinSeq-Locations \/ {(IC SCM+FSA )}) \/ NAT ) \/ Int-Locations by XBOOLE_1:4 ;
s . (insloc 0 ) = goto (insloc 0 ) by A3;
then s +* (IC s),(goto (IC s)) = s by A2, FUNCT_7:37;
then A7: not s is halting by SCMFSA6B:20;
A8: {(IC SCM+FSA )} c= dom s by A5, XBOOLE_1:7;
intloc 0 in Int-Locations by SCMFSA_2:9;
then intloc 0 in dom s by A6, XBOOLE_0:def 3;
then for x being set st x in {(intloc 0 )} holds
x in dom s by TARSKI:def 1;
then A9: {(intloc 0 )} c= dom s by TARSKI:def 3;
A10: dom (Initialized I) = ((dom I) \/ {(intloc 0 )}) \/ {(IC SCM+FSA )} by SCMFSA6A:43
.= {(intloc 0 )} \/ {(IC SCM+FSA )} by A1 ;
then A11: dom (Initialized I) c= dom s by A8, A9, XBOOLE_1:8;

now

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

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

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

hence (Initialized I) . x = 1 by SCMFSA6A:46
.= s . x by A3, A14 ;
:: 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;

then Initialized I c= s by A11, GRFUNC_1:8;
hence contradiction by A7, AMI_1:def 26; :: thesis: verum