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