let A be Matrix of REAL ; :: thesis: (- 1) * A = - A
A1:
len (- A) = len A
by MATRIX_3:def 2;
A2:
len ((- 1) * A) = len A
by Th5;
A3:
width (- A) = width A
by MATRIX_3:def 2;
A4:
width ((- 1) * A) = width A
by Th5;
now let i,
j be
Nat;
:: thesis: ( [i,j] in Indices ((- 1) * A) implies ((- 1) * A) * i,j = (- A) * i,j )assume A5:
[i,j] in Indices ((- 1) * A)
;
:: thesis: ((- 1) * A) * i,j = (- A) * i,jreconsider i0 =
i,
j0 =
j as
Element of
NAT by ORDINAL1:def 13;
( 1
<= i0 &
i0 <= len A & 1
<= j0 &
j0 <= width A )
by A2, A4, A5, MATRIXC1:1;
then A6:
[i0,j0] in Indices A
by MATRIXC1:1;
hence ((- 1) * A) * i,
j =
(- 1) * (A * i0,j0)
by A2, A4, Th3
.=
- (A * i,j)
.=
(- A) * i,
j
by A1, A3, A6, Lm3
;
:: thesis: verum end;
hence
(- 1) * A = - A
by A1, A2, A3, A4, MATRIX_1:21; :: thesis: verum