let M be Matrix of n,K; :: thesis: ( M is line_circulant implies M is subsymmetric )
assume M is line_circulant ; :: thesis: M is subsymmetric
then consider p being FinSequence of K such that
len p = width M and
A1: M is_line_circulant_about p by MATRIX16:def 2;
A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;
let i, j, k, l be Nat; :: according to MATRIX17:def 1 :: thesis: ( [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i implies M * (i,j) = M * (k,l) )
assume that
A3: [i,j] in Indices M and
A4: ( k = (n + 1) - j & l = (n + 1) - i ) ; :: thesis: M * (i,j) = M * (k,l)
( k in Seg n & l in Seg n ) by A3, A2, A4, Lm2;
then A5: [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
M * (k,l) = p . (((((n + 1) - i) - ((n + 1) - j)) mod (len p)) + 1) by A1, A2, A4, A5, MATRIX16:def 1
.= p . (((j - i) mod (len p)) + 1) ;
hence M * (i,j) = M * (k,l) by A3, A1, MATRIX16:def 1; :: thesis: verum