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