let M be Matrix of COMPLEX; (- 1) * M = - M
A1:
width (- M) = width M
by Th8;
A2:
width ((- 1) * M) = width M
by Th2;
A3:
len ((- 1) * M) = len M
by Th2;
A4:
now for i, j being Nat st [i,j] in Indices ((- 1) * M) holds
((- 1) * M) * (i,j) = (- M) * (i,j)let i,
j be
Nat;
( [i,j] in Indices ((- 1) * M) implies ((- 1) * M) * (i,j) = (- M) * (i,j) )assume A5:
[i,j] in Indices ((- 1) * M)
;
((- 1) * M) * (i,j) = (- M) * (i,j)then A6:
1
<= i
by Th1;
A7:
1
<= j
by A5, Th1;
A8:
j <= width M
by A2, A5, Th1;
i <= len M
by A3, A5, Th1;
then A9:
[i,j] in Indices M
by A6, A7, A8, Th1;
hence ((- 1) * M) * (
i,
j) =
(- 1) * (M * (i,j))
by Th3
.=
- (M * (i,j))
.=
(- M) * (
i,
j)
by A9, Th9
;
verum end;
len (- M) = len M
by Th8;
hence
(- 1) * M = - M
by A3, A1, A2, A4, MATRIX_0:21; verum