A1:
0. (K,1,1) = 1 |-> (1 |-> (0. K))
;
set M1 = 0. (K,1);
take p = 1 |-> (0. K); ( p is first-line-of-circulant & p is first-col-of-circulant )
A2:
len (1 |-> (0. K)) = 1
by CARD_1:def 7;
A3:
Indices (0. (K,1)) = [:(Seg 1),(Seg 1):]
by MATRIX_0:24;
A4:
for i, j being Nat st [i,j] in Indices (0. (K,1)) holds
(0. (K,1)) * (i,j) = p . (((i - j) mod (len p)) + 1)
proof
let i,
j be
Nat;
( [i,j] in Indices (0. (K,1)) implies (0. (K,1)) * (i,j) = p . (((i - j) mod (len p)) + 1) )
assume A5:
[i,j] in Indices (0. (K,1))
;
(0. (K,1)) * (i,j) = p . (((i - j) mod (len p)) + 1)
then
((i - j) mod 1) + 1
in Seg 1
by A3, Lm3;
then
((Seg 1) --> (0. K)) . (((i - j) mod 1) + 1) = 0. K
by FUNCOP_1:7;
hence
(0. (K,1)) * (
i,
j)
= p . (((i - j) mod (len p)) + 1)
by A2, A1, A5, MATRIX_3:1;
verum
end;
A6:
for i, j being Nat st [i,j] in Indices (0. (K,1)) holds
(0. (K,1)) * (i,j) = p . (((j - i) mod (len p)) + 1)
proof
let i,
j be
Nat;
( [i,j] in Indices (0. (K,1)) implies (0. (K,1)) * (i,j) = p . (((j - i) mod (len p)) + 1) )
assume A7:
[i,j] in Indices (0. (K,1))
;
(0. (K,1)) * (i,j) = p . (((j - i) mod (len p)) + 1)
then
((j - i) mod 1) + 1
in Seg 1
by A3, Lm3;
then
((Seg 1) --> (0. K)) . (((j - i) mod 1) + 1) = 0. K
by FUNCOP_1:7;
hence
(0. (K,1)) * (
i,
j)
= p . (((j - i) mod (len p)) + 1)
by A2, A1, A7, MATRIX_3:1;
verum
end;
width (0. (K,1)) = 1
by MATRIX_0:24;
then
0. (K,1) is_line_circulant_about p
by A2, A6;
hence
p is first-line-of-circulant
by A2; p is first-col-of-circulant
len (0. (K,1)) = 1
by MATRIX_0:24;
then
0. (K,1) is_col_circulant_about p
by A2, A4;
hence
p is first-col-of-circulant
by A2; verum