set M1 = (n,n) --> a;
set p = n |-> a;
A4: ( len ((n,n) --> a) = n & len (n |-> a) = n ) by CARD_1:def 7;
A5: Indices ((n,n) --> a) = [:(Seg n),(Seg n):] by MATRIX_0:24;
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 CARD_1:def 7;
then ((Seg n) --> a) . (((i - j) mod (len (n |-> a))) + 1) = a by FUNCOP_1:7;
hence ((n,n) --> a) * (i,j) = (n |-> a) . (((i - j) mod (len (n |-> a))) + 1) by A6, MATRIX_0:46; :: thesis: verum

end;

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