for i, j being Nat st [i,j] in Indices ((n,n) --> (- 1)) holds
((n,n) --> (- 1)) * (i,j) < 0

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((n,n) --> (- 1)) implies ((n,n) --> (- 1)) * (i,j) < 0 )
assume [i,j] in Indices ((n,n) --> (- 1)) ; :: thesis: ((n,n) --> (- 1)) * (i,j) < 0
then ((n,n) --> (- 1)) * (i,j) = - 1 by MATRIX_2:1;
hence ((n,n) --> (- 1)) * (i,j) < 0 ; :: thesis: verum

end;

hence for b₁ being Matrix of n, REAL st b₁ = (n,n) --> (- 1) holds
b₁ is Negative by Def2; :: thesis: verum