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

per cases ( a in {(intloc 0)} or a in {(IC )} ) by A3, A2, XBOOLE_0:def 3;

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

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

end;

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

then a = IC by TARSKI:def 1;
hence contradiction by SCMFSA_2:56; :: thesis: verum

end;

end;