let p be preProgram of SCM+FSA; :: thesis: not FirstNotUsed p in UsedILoc p
consider sil being finite Subset of Int-Locations such that
A1: sil = (UsedILoc p) \/ {(intloc 0)} and
A2: FirstNotUsed p = FirstNotIn sil by Def7;
not FirstNotUsed p in sil by A2, SCMFSA_M:14;
hence not FirstNotUsed p in UsedILoc p by A1, XBOOLE_0:def 3; :: thesis: verum