take p = 1 |-> (0. K); :: thesis: ( p is first-line-of-circulant & p is first-col-of-circulant )
A2: ( Indices (0. K,1) = [:(Seg 1),(Seg 1):] & len (0. K,1) = 1 & width (0. K,1) = 1 ) by MATRIX_1:25;
A3: len (1 |-> (0. K)) = 1 by FINSEQ_2:69;
A4: ( 0. K,1 = 1 |-> (1 |-> (0. K)) & 0. K,1,1 = 1 |-> (1 |-> (0. K)) ) ;
set M1 = 0. K,1;
thus p is first-line-of-circulant :: thesis: p is first-col-of-circulant

proof

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 B1: [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 A2, Lm2;
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 A3, B1, A4, MATRIX_3:3; :: thesis: verum

end;

then 0. K,1 is_line_circulant_about p by A2, A3, Def1;
hence p is first-line-of-circulant by A3, Def3; :: thesis: verum

end;

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 B1: [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 A2, Lm2;
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 A3, B1, A4, MATRIX_3:3; :: thesis: verum

end;

then 0. K,1 is_col_circulant_about p by A2, A3, Def4;
hence p is first-col-of-circulant by A3, Def6; :: thesis: verum