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

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