let A be Matrix of REAL; (- 1) * A = - A
A1:
width ((- 1) * A) = width A
by Th5;
A2:
len ((- 1) * A) = len A
by Th5;
A3:
now 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;
( [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)
;
((- 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
;
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; verum