len p = n by FINSEQ_1:def 18;
hence <*p*> is Matrix of 1,n,D by MATRIX_1:11; :: thesis: verum