set p = the m -element FinSequence of D;
take the m -element FinSequence of D ; :: thesis: ( the m -element FinSequence of D is m -element & the m -element FinSequence of D is D -valued )
thus ( the m -element FinSequence of D is m -element & the m -element FinSequence of D is D -valued ) ; :: thesis: verum