for i, j being Nat st [i,j] in Indices (n,n --> 1) holds
(n,n --> 1) * i,j > 0 by MATRIX_2:1;
hence n,n --> 1 is Positive Matrix of n, REAL by Def1; :: thesis: verum