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 A1:
( M1 is_anti-circular_about p & n > 0 )
; :: thesis: p = Line M1,1
A2:
( len M1 = n & width M1 = n )
by MATRIX_1:25;
then A4:
( len (Line M1,1) = n & dom p = Seg (len p) & len p = n )
by A1, Def10, FINSEQ_1:def 3, MATRIX_1:def 8;
then A5:
dom (Line M1,1) = dom p
by FINSEQ_1:def 3;
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 B1:
k in dom p
;
:: thesis: p . k = (Line M1,1) . k
then B3:
k in Seg (width M1)
by A4, MATRIX_1:def 8;
n >= 0 + 1
by A1, INT_1:20;
then B5:
1
in Seg n
;
B7:
( 1
<= k &
k <= n )
by B1, A4, FINSEQ_1:3;
[1,k] in [:(Seg n),(Seg n):]
by B1, A4, B5, ZFMISC_1:def 2;
then B8:
[1,k] in Indices M1
by MATRIX_1:25;
(Line M1,1) . k =
M1 * 1,
k
by B3, MATRIX_1:def 8
.=
p . (((k - 1) mod (len p)) + 1)
by A1, Def10, B8, B7
.=
p . (((k - 1) mod n) + 1)
by A1, A2, Def10
.=
p . ((k - 1) + 1)
by B7, Lm1
;
hence
p . k = (Line M1,1) . k
;
:: thesis: verum
end;
hence
p = Line M1,1
by A5, FINSEQ_1:17; :: thesis: verum