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

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 Element of NAT by ORDINAL1:def 13;
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_1:21; :: thesis: verum