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