n in NAT by ORDINAL1:def 12;
hence M @ is Matrix of n,D by Lm2; :: thesis: verum