for X being FinSequence-membered set ex Y being non empty set st X c= Y *