let L be finite Subset of FinSeq-Locations ; :: thesis: not First*NotIn L in L
set FNI = First*NotIn L;
consider sn being non empty Subset of NAT such that
A1: First*NotIn L = fsloc (min sn) and
A2: sn = { k where k is Element of NAT : not fsloc k in L } by Def8;
min sn in sn by XXREAL_2:def 7;
then consider k being Element of NAT such that
A3: ( k = min sn & not fsloc k in L ) by A2;
thus not First*NotIn L in L by A1, A3; :: thesis: verum