consider sil being finite Subset of Int-Locations such that
A1: sil = (UsedILoc p) \/ {(intloc 0)} and
A2: FirstNotUsed p = FirstNotIn sil by Def7;

now :: thesis: not FirstNotIn sil = intloc 0

assume FirstNotIn sil = intloc 0 ; :: thesis: contradiction
then not intloc 0 in sil by SCMFSA_M:14;
hence contradiction by A1, ZFMISC_1:136; :: thesis: verum

end;

hence not FirstNotUsed p is read-only by A2, SCMFSA_M:def 2; :: thesis: verum