set p = n |-> a;
A2: ( width (n,n --> a) = n & len (n,n --> a) = n & Indices (n,n --> a) = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
A3: len (n |-> a) = n by FINSEQ_1:def 18;
set M1 = n,n --> a;
for i, j being Nat st [i,j] in Indices (n,n --> a) holds
(n,n --> a) * i,j = (n |-> a) . (((i - j) mod (len (n |-> a))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (n,n --> a) implies (n,n --> a) * i,j = (n |-> a) . (((i - j) mod (len (n |-> a))) + 1) )
assume B1: [i,j] in Indices (n,n --> a) ; :: thesis: (n,n --> a) * i,j = (n |-> a) . (((i - j) mod (len (n |-> a))) + 1)
then ((i - j) mod n) + 1 in Seg n by A2, Lm2;
then ((i - j) mod (len (n |-> a))) + 1 in Seg n by FINSEQ_1:def 18;
then ((Seg n) --> a) . (((i - j) mod (len (n |-> a))) + 1) = a by FUNCOP_1:13;
hence (n,n --> a) * i,j = (n |-> a) . (((i - j) mod (len (n |-> a))) + 1) by B1, MATRIX_2:1; :: thesis: verum

end;

then n,n --> a is_col_circulant_about n |-> a by A2, A3, Def4;
hence for b₁ being Matrix of n,K st b₁ = n,n --> a holds
b₁ is col_circulant by Def5, A2, A3; :: thesis: verum