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