A1: 0. (K,1,1) = 1 |-> (1 |-> (0. K)) ;
set M1 = 0. (K,1);
take p = 1 |-> (0. K); :: thesis: ( 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; :: thesis: ( [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)) ; :: thesis: (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; :: thesis: 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; :: thesis: ( [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)) ; :: thesis: (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; :: thesis: 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; :: thesis: 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; :: thesis: verum