let M1, M2 be Matrix of len p,K; ( M1 is_col_circulant_about p & M2 is_col_circulant_about p implies M1 = M2 )
assume that
A2:
M1 is_col_circulant_about p
and
A3:
M2 is_col_circulant_about p
; M1 = M2
A4:
Indices M1 = Indices M2
by MATRIX_0:26;
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)
proof
let i,
j be
Nat;
( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A5:
[i,j] in Indices M1
;
M1 * (i,j) = M2 * (i,j)
then
M1 * (
i,
j)
= p . (((i - j) mod (len p)) + 1)
by A2;
hence
M1 * (
i,
j)
= M2 * (
i,
j)
by A3, A4, A5;
verum
end;
hence
M1 = M2
by MATRIX_0:27; verum