for X being set
for f being FinSequence of X
for g being Subset of f st len (Seq g) = len f holds
Seq g = f