for S being 1-sorted
for p being FinSequence st ( for i being Nat st i in dom p holds
p . i in S ) holds
p is FinSequence of S