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

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

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

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

end;

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

then f = IC by TARSKI:def 1;
hence contradiction by SCMFSA_2:57; :: thesis: verum

end;

end;