let M1, M2 be Matrix of n,K; ( ( for i, j being Nat st [i,j] in Indices A holds
M1 * (i,j) = - (A * (i,j)) ) & ( for i, j being Nat st [i,j] in Indices A holds
M2 * (i,j) = - (A * (i,j)) ) implies M1 = M2 )
assume that
A16:
for i, j being Nat st [i,j] in Indices A holds
M1 * (i,j) = - (A * (i,j))
and
A17:
for i, j being Nat st [i,j] in Indices A holds
M2 * (i,j) = - (A * (i,j))
; M1 = M2
A18:
now for i, j being Nat st [i,j] in Indices A holds
M1 * (i,j) = M2 * (i,j)let i,
j be
Nat;
( [i,j] in Indices A implies M1 * (i,j) = M2 * (i,j) )assume A19:
[i,j] in Indices A
;
M1 * (i,j) = M2 * (i,j)then
M1 * (
i,
j)
= - (A * (i,j))
by A16;
hence
M1 * (
i,
j)
= M2 * (
i,
j)
by A17, A19;
verum end;
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then
Indices A = Indices M1
by MATRIX_0:24;
hence
M1 = M2
by A18, MATRIX_0:27; verum