let M be Matrix of n,REAL; :: thesis: ( M = (n,n) --> (- 1) implies M is Negative )
assume A1: M = (n,n) --> (- 1) ; :: thesis: M is Negative
let i be Nat; :: according to MATRIX10:def 2 :: thesis: for j being Nat st [i,j] in Indices M holds
M * (i,j) < 0
let j be Nat; :: thesis: ( [i,j] in Indices M implies M * (i,j) < 0 )
assume [i,j] in Indices M ; :: thesis: M * (i,j) < 0
then M * (i,j) = - 1 by A1, MATRIX_0:46, Lm2;
hence M * (i,j) < 0 ; :: thesis: verum