theorem Th1: :: NEWTON02:103

for D being set
for f being FinSequence holds
( f is D -valued iff f is FinSequence of D )