theorem Th9: :: NDIFF_5:9

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