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