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