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 Element of NAT by A2;
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;