for X being non-empty FinSequence
for x being set st x in product X holds
x is FinSequence