set p = the m -element FinSequence of D;
reconsider pp = the m -element FinSequence of D as Element of D * by FINSEQ_1:def 11;
take pp ; :: thesis: pp is m -element
thus pp is m -element ; :: thesis: verum