let p be preProgram of SCM+FSA; :: thesis: not First*NotUsed p in UsedI*Loc p

ex sil being finite Subset of FinSeq-Locations st

( sil = UsedI*Loc p & First*NotUsed p = First*NotIn sil ) by Def8;

hence not First*NotUsed p in UsedI*Loc p by SCMFSA_M:16; :: thesis: verum

ex sil being finite Subset of FinSeq-Locations st

( sil = UsedI*Loc p & First*NotUsed p = First*NotIn sil ) by Def8;

hence not First*NotUsed p in UsedI*Loc p by SCMFSA_M:16; :: thesis: verum