set M1 = n,n --> a;
set p = n |-> a;
A4: ( len (n,n --> a) = n & len (n |-> a) = n ) by FINSEQ_1:def 18, MATRIX_1:25;
A5: Indices (n,n --> a) = [:(Seg n),(Seg n):] by MATRIX_1:25;
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 A6: [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 A5, Lm3;
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 A6, MATRIX_2:1; :: thesis: verum

end;

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