let M be Matrix of n,K; :: thesis: ( M is col_circulant implies M is subsymmetric )
assume M is col_circulant ; :: thesis: M is subsymmetric
then consider p being FinSequence of K such that
A1: len p = len M and
A2: M is_col_circulant_about p by MATRIX16:def 5;
A3: len M = n by MATRIX_1:24;
A4: Indices M = [:(Seg n),(Seg n):] by MATRIX_1: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
A5: [i,j] in Indices M and
A6: ( k = (n + 1) - j & l = (n + 1) - i ) ; :: thesis: M * (i,j) = M * (k,l)
( k in Seg n & l in Seg n ) by A5, A4, A6, Lm2;
then A7: [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
M * (k,l) = p . (((((n + 1) - j) - ((n + 1) - i)) mod n) + 1) by A1, A2, A3, A4, A6, A7, MATRIX16:def 4
.= p . (((i - j) mod n) + 1) ;
hence M * (i,j) = M * (k,l) by A1, A2, A3, A5, MATRIX16:def 4; :: thesis: verum