let A be Matrix of REAL; :: thesis: (- 1) * A = - A
A1: width ((- 1) * A) = width A by Th5;
A2: len ((- 1) * A) = len A by Th5;

A3: now :: thesis: for i, j being Nat st [i,j] in Indices ((- 1) * A) holds
((- 1) * A) * (i,j) = (- A) * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in Indices ((- 1) * A) implies ((- 1) * A) * (i,j) = (- A) * (i,j) )
reconsider i0 = i, j0 = j as Nat ;
assume A4: [i,j] in Indices ((- 1) * A) ; :: thesis: ((- 1) * A) * (i,j) = (- A) * (i,j)
then A5: ( 1 <= j0 & j0 <= width A ) by A1, MATRIXC1:1;
( 1 <= i0 & i0 <= len A ) by A2, A4, MATRIXC1:1;
then A6: [i0,j0] in Indices A by A5, MATRIXC1:1;
hence ((- 1) * A) * (i,j) = (- 1) * (A * (i0,j0)) by Th3
.= - (A * (i,j))
.= (- A) * (i,j) by A6, Lm3 ;
:: thesis: verum

end;

( len (- A) = len A & width (- A) = width A ) by MATRIX_3:def 2;
hence (- 1) * A = - A by A2, A1, A3, MATRIX_0:21; :: thesis: verum