let n be Element of NAT ; :: thesis: for K being Field
for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_anti-circular_about p & n > 0 holds
p = Line (M1,1)
let K be Field; :: thesis: for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_anti-circular_about p & n > 0 holds
p = Line (M1,1)
let p be FinSequence of K; :: thesis: for M1 being Matrix of n,K st M1 is_anti-circular_about p & n > 0 holds
p = Line (M1,1)
let M1 be Matrix of n,K; :: thesis: ( M1 is_anti-circular_about p & n > 0 implies p = Line (M1,1) )
assume that
A1: M1 is_anti-circular_about p and
A2: n > 0 ; :: thesis: p = Line (M1,1)
A3: dom p = Seg (len p) by FINSEQ_1:def 3;
A4: width M1 = n by MATRIX_0:24;
then A5: len p = n by A1;
A6: for k being Nat st k in dom p holds
p . k = (Line (M1,1)) . k

proof

let k be Nat; :: thesis: ( k in dom p implies p . k = (Line (M1,1)) . k )
assume A7: k in dom p ; :: thesis: p . k = (Line (M1,1)) . k
then A8: 1 <= k by A3, FINSEQ_1:1;
n >= 0 + 1 by A2, INT_1:7;
then 1 in Seg n ;
then [1,k] in [:(Seg n),(Seg n):] by A3, A5, A7, ZFMISC_1:def 2;
then A9: [1,k] in Indices M1 by MATRIX_0:24;
A10: k <= n by A3, A5, A7, FINSEQ_1:1;
(Line (M1,1)) . k = M1 * (1,k) by A4, A3, A5, A7, MATRIX_0:def 7
.= p . (((k - 1) mod (len p)) + 1) by A1, A8, A9
.= p . (((k - 1) mod n) + 1) by A1, A4
.= p . ((k - 1) + 1) by A8, A10, Lm1 ;
hence p . k = (Line (M1,1)) . k ; :: thesis: verum

end;

len (Line (M1,1)) = n by A4, MATRIX_0:def 7;
then dom (Line (M1,1)) = dom p by A3, A5, FINSEQ_1:def 3;
hence p = Line (M1,1) by A6, FINSEQ_1:13; :: thesis: verum