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 for b₁ being Matrix of n, REAL st b₁ = (n,n) --> (- 1) holds
b₁ is Nonpositive by Def3; :: thesis: verum