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

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

suppose A3: a in dom I ; :: thesis: contradiction

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

end;

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

hence contradiction by A1, TARSKI:def 1; :: thesis: verum

end;

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

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

end;

end;