for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location holds {aa,bb,c} c= UsedILoc (FinSeqMin (f,aa,bb,c))