set p = n |-> a;
A1:
( width ((n,n) --> a) = n & len (n |-> a) = n )
by CARD_1:def 7, MATRIX_0:24;
A2:
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) . (((j - i) mod (len (n |-> a))) + 1)
proof
let i,
j be
Nat;
( [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)
;
((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 CARD_1:def 7;
then
((Seg n) --> a) . (((j - i) mod (len (n |-> a))) + 1) = a
by FUNCOP_1:7;
hence
((n,n) --> a) * (
i,
j)
= (n |-> a) . (((j - i) mod (len (n |-> a))) + 1)
by A3, MATRIX_0:46;
verum
end;
then
(n,n) --> a is_line_circulant_about n |-> a
by A1;
hence
for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is line_circulant
; verum