set p = n |-> (0. K);
A1: len (0. (K,n)) = n by MATRIX_0:24;
A2: 0. (K,n,n) = n |-> (n |-> (0. K)) ;
set M1 = 0. (K,n);
A3: len (n |-> (0. K)) = n by CARD_1:def 7;
A4: Indices (0. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
for i, j being Nat st [i,j] in Indices (0. (K,n)) holds
(0. (K,n)) * (i,j) = (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (0. (K,n)) implies (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1) )
assume A5: [i,j] in Indices (0. (K,n)) ; :: thesis: (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1)
then ((i - j) mod n) + 1 in Seg n by A4, Lm3;
then ((i - j) mod (len (n |-> (0. K)))) + 1 in Seg n by CARD_1:def 7;
then ((Seg n) --> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1) = 0. K by FUNCOP_1:7;
hence (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1) by A2, A5, MATRIX_3:1; :: thesis: verum

end;

then A6: 0. (K,n) is_col_circulant_about n |-> (0. K) by A1, A3;
A7: width (0. (K,n)) = n by MATRIX_0:24;
thus 0. (K,n) is line_circulant :: thesis: 0. (K,n) is col_circulant

proof

for i, j being Nat st [i,j] in Indices (0. (K,n)) holds
(0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (0. (K,n)) implies (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1) )
assume A8: [i,j] in Indices (0. (K,n)) ; :: thesis: (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1)
then ((j - i) mod n) + 1 in Seg n by A4, Lm3;
then ((Seg n) --> (0. K)) . (((j - i) mod n) + 1) = 0. K by FUNCOP_1:7;
hence (0. (K,n)) * (i,j) = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1) by A3, A2, A8, MATRIX_3:1; :: thesis: verum

end;

then 0. (K,n) is_line_circulant_about n |-> (0. K) by A7, A3;
then consider p being FinSequence of K such that
A9: ( len p = width (0. (K,n)) & 0. (K,n) is_line_circulant_about p ) ;
take p ; :: according to MATRIX16:def 2 :: thesis: ( len p = width (0. (K,n)) & 0. (K,n) is_line_circulant_about p )
thus ( len p = width (0. (K,n)) & 0. (K,n) is_line_circulant_about p ) by A9; :: thesis: verum

end;

consider p being FinSequence of K such that
A10: ( len p = len (0. (K,n)) & 0. (K,n) is_col_circulant_about p ) by A6;
take p ; :: according to MATRIX16:def 5 :: thesis: ( len p = len (0. (K,n)) & 0. (K,n) is_col_circulant_about p )
thus ( len p = len (0. (K,n)) & 0. (K,n) is_col_circulant_about p ) by A10; :: thesis: verum