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 FINSEQ_1:def 18;
A3: Indices (0. K,1) = [:(Seg 1),(Seg 1):] by MATRIX_1:25;
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:13;
hence (0. K,1) * i,j = p . (((i - j) mod (len p)) + 1) by A2, A1, A5, MATRIX_3:3; :: 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:13;
hence (0. K,1) * i,j = p . (((j - i) mod (len p)) + 1) by A2, A1, A7, MATRIX_3:3; :: thesis: verum

end;

width (0. K,1) = 1 by MATRIX_1:25;
then 0. K,1 is_line_circulant_about p by A2, A6, Def1;
hence p is first-line-of-circulant by A2, Def3; :: thesis: p is first-col-of-circulant
len (0. K,1) = 1 by MATRIX_1:25;
then 0. K,1 is_col_circulant_about p by A2, A4, Def4;
hence p is first-col-of-circulant by A2, Def6; :: thesis: verum