A2: ( Indices (0. K,n) = [:(Seg n),(Seg n):] & len (0. K,n) = n & width (0. K,n) = n ) by MATRIX_1:25;
A3: len (n |-> (0. K)) = n by FINSEQ_1:def 18;
A4: ( 0. K,n = n |-> (n |-> (0. K)) & 0. K,n,n = n |-> (n |-> (0. K)) ) ;
set p = n |-> (0. K);
set M1 = 0. K,n;
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 B1: [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 A2, Lm2;
then ((Seg n) --> (0. K)) . (((j - i) mod n) + 1) = 0. K by FUNCOP_1:13;
hence (0. K,n) * i,j = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1) by A3, B1, A4, MATRIX_3:3; :: thesis: verum

end;

then A9: 0. K,n is_line_circulant_about n |-> (0. K) by A2, A3, Def1;
consider p being FinSequence of K such that
A11: ( len p = width (0. K,n) & 0. K,n is_line_circulant_about p ) by A2, A3, A9;
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 A11; :: thesis: verum

end;

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 B1: [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 A2, Lm2;
then ((i - j) mod (len (n |-> (0. K)))) + 1 in Seg n by FINSEQ_1:def 18;
then ((Seg n) --> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1) = 0. K by FUNCOP_1:13;
hence (0. K,n) * i,j = (n |-> (0. K)) . (((i - j) mod (len (n |-> (0. K)))) + 1) by B1, A4, MATRIX_3:3; :: thesis: verum

end;

then A9: 0. K,n is_col_circulant_about n |-> (0. K) by A2, A3, Def4;
consider p being FinSequence of K such that
A11: ( len p = len (0. K,n) & 0. K,n is_col_circulant_about p ) by A2, A3, A9;
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 A11; :: thesis: verum