let n be Element of NAT ; 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; 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; 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; ( 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
; 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;
( k in dom p implies p . k = (Line (M1,1)) . k )
assume A7:
k in dom p
;
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
;
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; verum