take the FinSequence of D ; :: thesis: the FinSequence of D is D -valued
thus the FinSequence of D is D -valued ; :: thesis: verum