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