let I be Program of SCM+FSA ; :: thesis: for f being FinSeq-Location holds not f in dom (Initialized I)
let f be FinSeq-Location ; :: thesis: not f in dom (Initialized I)
assume f in dom (Initialized I) ; :: thesis: contradiction
then f in ((dom I) \/ {(intloc 0 )}) \/ {(IC SCM+FSA )} by Th43;
then A1: ( f in (dom I) \/ {(intloc 0 )} or f in {(IC SCM+FSA )} ) by XBOOLE_0:def 3;

per cases ( f in dom I or f in {(intloc 0 )} or f in {(IC SCM+FSA )} ) by A1, XBOOLE_0:def 3;

suppose A2: f in dom I ; :: thesis: contradiction

dom I c= NAT by RELAT_1:def 18;
then reconsider f = f as Instruction-Location of SCM+FSA by A2, AMI_1:def 4;
f in dom I by A2;
hence contradiction by SCMFSA_2:85; :: thesis: verum

end;

suppose f in {(intloc 0 )} ; :: thesis: contradiction

then f = intloc 0 by TARSKI:def 1;
hence contradiction by SCMFSA_2:83; :: thesis: verum

end;

suppose f in {(IC SCM+FSA )} ; :: thesis: contradiction

then f = IC SCM+FSA by TARSKI:def 1;
hence contradiction by SCMFSA_2:82; :: thesis: verum

end;

end;