environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, VECTSP_1, FINSEQ_1, MATRIX_1, NAT_1, XXREAL_0, ARYTM_1, INT_1, ARYTM_3, CARD_1, ZFMISC_1, FUNCT_1, RELAT_1, STRUCT_0, ALGSTR_0, FUNCOP_1, FVSUM_1, SUPINF_2, FINSEQ_2, TREES_1, XBOOLE_0, QC_LANG1, PARTFUN1, MATRIX16, RELAT_2, GROUP_1, MATRIX17;
notations HIDDEN, MATRIX_0, VECTSP_1, GROUP_1, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, TARSKI, FINSEQ_1, FINSEQ_2, FVSUM_1, FUNCT_1, STRUCT_0, BINOP_1, XXREAL_0, FUNCOP_1, INT_1, NUMBERS, MATRIX_1, MATRIX_3, XCMPLX_0, MATRIX_4, MATRIX_6, RELAT_1, ALGSTR_0, PARTFUN1, MATRIX13, MATRIX16, RLVECT_1;
definitions MATRIX_6;
theorems MATRIX_5, MATRIX_3, FINSEQ_1, FUNCT_1, ZFMISC_1, POLYNOM1, CARD_1, INT_1, VECTSP_1, FVSUM_1, MATRIX_0, FINSEQ_2, FUNCOP_1, MATRIXR1, XREAL_1, XXREAL_0, PARTFUN1, MATRIX16, RLVECT_1, NAT_D, ORDINAL1;
schemes ;
registrations STRUCT_0, INT_1, RELSET_1, VECTSP_1, FINSEQ_2, XXREAL_0, XREAL_0, ORDINAL1, MATRIX_6, MATRIX_0, MATRIX_1;
constructors HIDDEN, REAL_1, MATRIX_6, XXREAL_0, MATRIX13, POLYNOM1, BINOP_2, FVSUM_1, MATRIX16, MATRIX_4, MATRIX_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities FVSUM_1, MATRIX_4, FINSEQ_1, FINSEQ_2, ALGSTR_0;
expansions MATRIX_6;
Lm1:
for n, i being Nat st i in Seg n holds
(n + 1) - i in Seg n
Lm2:
for n, i, j being Nat st [i,j] in [:(Seg n),(Seg n):] holds
( (n + 1) - j in Seg n & (n + 1) - i in Seg n )
Lm3:
for n, i, j being Nat st i in Seg n & j in Seg n & i + j <> n + 1 holds
((i + j) - 1) mod n in Seg n
Lm4:
for n, i, j being Nat st [i,j] in [:(Seg n),(Seg n):] & i + j <> n + 1 holds
((i + j) - 1) mod n in Seg n