set p = n |-> (0. K);
A1: width (0. K,n) = n by MATRIX_1:25;
A2: 0. K,n,n = n |-> (n |-> (0. K)) ;
set M1 = 0. K,n;
A3: len (n |-> (0. K)) = n by FINSEQ_1:def 18;
A4: Indices (0. K,n) = [:(Seg n),(Seg n):] by MATRIX_1:25;
A5: for i, j being Nat st [i,j] in Indices (0. K,n) & i >= j holds
(0. K,n) * i,j = (- (n |-> (0. K))) . (((j - i) mod (len (n |-> (0. K)))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (0. K,n) & i >= j implies (0. K,n) * i,j = (- (n |-> (0. K))) . (((j - i) mod (len (n |-> (0. K)))) + 1) )
assume that
A6: [i,j] in Indices (0. K,n) and
i >= j ; :: thesis: (0. K,n) * i,j = (- (n |-> (0. K))) . (((j - i) mod (len (n |-> (0. K)))) + 1)
A7: ((j - i) mod n) + 1 in Seg n by A4, A6, Lm3;
(- (n |-> (0. K))) . (((j - i) mod (len (n |-> (0. K)))) + 1) = (n |-> (- (0. K))) . (((j - i) mod n) + 1) by A3, FVSUM_1:34
.= - (0. K) by A7, FUNCOP_1:13
.= 0. K by VECTSP_2:34 ;
hence (0. K,n) * i,j = (- (n |-> (0. K))) . (((j - i) mod (len (n |-> (0. K)))) + 1) by A2, A6, MATRIX_3:3; :: thesis: verum

end;

for i, j being Nat st [i,j] in Indices (0. K,n) & i <= j holds
(0. K,n) * i,j = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (0. K,n) & i <= j implies (0. K,n) * i,j = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1) )
assume that
A8: [i,j] in Indices (0. K,n) and
i <= j ; :: thesis: (0. K,n) * i,j = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1)
((j - i) mod n) + 1 in Seg n by A4, A8, Lm3;
then ((Seg n) --> (0. K)) . (((j - i) mod n) + 1) = 0. K by FUNCOP_1:13;
hence (0. K,n) * i,j = (n |-> (0. K)) . (((j - i) mod (len (n |-> (0. K)))) + 1) by A3, A2, A8, MATRIX_3:3; :: thesis: verum

end;

then 0. K,n is_anti-circular_about n |-> (0. K) by A1, A3, A5, Def9;
then consider p being FinSequence of K such that
A9: ( len p = width (0. K,n) & 0. K,n is_anti-circular_about p ) by A1, A3;
take p ; :: according to MATRIX16:def 10 :: thesis: ( len p = width (0. K,n) & 0. K,n is_anti-circular_about p )
thus ( len p = width (0. K,n) & 0. K,n is_anti-circular_about p ) by A9; :: thesis: verum