let M1, M2 be Matrix of n,K; ( ( for i being Nat st [i,i] in Indices M1 holds
M1 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M1 & i <> j holds
M1 * (i,j) = 0. K ) & ( for i being Nat st [i,i] in Indices M2 holds
M2 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M2 & i <> j holds
M2 * (i,j) = 0. K ) implies M1 = M2 )
assume that
A3:
for i being Nat st [i,i] in Indices M1 holds
M1 * (i,i) = 1. K
and
A4:
for i, j being Nat st [i,j] in Indices M1 & i <> j holds
M1 * (i,j) = 0. K
and
A5:
for i being Nat st [i,i] in Indices M2 holds
M2 * (i,i) = 1. K
and
A6:
for i, j being Nat st [i,j] in Indices M2 & i <> j holds
M2 * (i,j) = 0. K
; M1 = M2
A7:
Indices M1 = Indices M2
by MATRIX_0:26;
A8:
now for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)let i,
j be
Nat;
( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )assume A9:
[i,j] in Indices M1
;
M1 * (i,j) = M2 * (i,j)A10:
now ( i <> j implies M1 * (i,j) = M2 * (i,j) )assume A11:
i <> j
;
M1 * (i,j) = M2 * (i,j)then
M1 * (
i,
j)
= 0. K
by A4, A9;
hence
M1 * (
i,
j)
= M2 * (
i,
j)
by A7, A6, A9, A11;
verum end; now ( i = j implies M1 * (i,j) = M2 * (i,j) )assume A12:
i = j
;
M1 * (i,j) = M2 * (i,j)then
M1 * (
i,
j)
= 1. K
by A3, A9;
hence
M1 * (
i,
j)
= M2 * (
i,
j)
by A7, A5, A9, A12;
verum end; hence
M1 * (
i,
j)
= M2 * (
i,
j)
by A10;
verum end;
A13:
( len M2 = n & width M2 = n )
by MATRIX_0:24;
( len M1 = n & width M1 = n )
by MATRIX_0:24;
hence
M1 = M2
by A8, A13, MATRIX_0:21; verum