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
A6: len p = len M and
A7: M is_col_circulant_about p by MATRIX16:def 5;
A8: len M = n by MATRIX_0:24;
A9: 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
A10: [i,j] in Indices M and
A11: ( k = (n + 1) - j & l = (n + 1) - i ) ; :: thesis: M * (i,j) = M * (k,l)
( k in Seg n & l in Seg n ) by A10, A9, A11, Lm2;
then A12: [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 A6, A7, A8, A9, A11, A12, MATRIX16:def 4
.= p . (((i - j) mod n) + 1) ;
hence M * (i,j) = M * (k,l) by A6, A7, A8, A10, MATRIX16:def 4; :: thesis: verum