theorem Th0: :: NEWTON04:2

for f being FinSequence ex D being non empty set st f is FinSequence of D