set p = n |-> a;
A1: ( width (n,n --> a) = n & len (n |-> a) = n ) by FINSEQ_1:def 18, MATRIX_1:25;
A2: 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) . (((j - i) 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) . (((j - i) mod (len (n |-> a))) + 1) )
assume A3: [i,j] in Indices (n,n --> a) ; :: thesis: (n,n --> a) * i,j = (n |-> a) . (((j - i) mod (len (n |-> a))) + 1)
then ((j - i) mod n) + 1 in Seg n by A2, Lm3;
then ((j - i) mod (len (n |-> a))) + 1 in Seg n by FINSEQ_1:def 18;
then ((Seg n) --> a) . (((j - i) mod (len (n |-> a))) + 1) = a by FUNCOP_1:13;
hence (n,n --> a) * i,j = (n |-> a) . (((j - i) mod (len (n |-> a))) + 1) by A3, MATRIX_2:1; :: thesis: verum

end;

then n,n --> a is_line_circulant_about n |-> a by A1, Def1;
hence for b₁ being Matrix of n,K st b₁ = n,n --> a holds
b₁ is line_circulant by A1, Def2; :: thesis: verum