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, GROUP_1, RELAT_1, FUNCT_1, TARSKI, STRUCT_0, ALGSTR_0, FUNCOP_1, FVSUM_1, SUPINF_2, FINSEQ_2, TREES_1, XBOOLE_0, QC_LANG1, INCSP_1, PARTFUN1, MESFUNC1, MATRIX16;
notations HIDDEN, MATRIX_0, VECTSP_1, GROUP_1, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, TARSKI, FINSEQ_1, FINSEQ_2, FVSUM_1, FUNCT_1, STRUCT_0, BINOP_1, XXREAL_0, MATRIX_1, FUNCOP_1, INT_1, NUMBERS, XCMPLX_0, MATRIX_3, MATRIX_4, MATRIX_6, RELAT_1, ALGSTR_0, PARTFUN1, MATRIX13;
definitions ;
theorems MATRIX_5, MATRIX_3, FINSEQ_1, FUNCT_1, ZFMISC_1, POLYNOM1, NAT_1, RLVECT_1, INT_1, VECTSP_1, FVSUM_1, MATRIX_0, FINSEQ_2, FUNCOP_1, MATRIXR1, XREAL_1, XXREAL_0, VECTSP_2, PARTFUN1, FINTOPO5, CARD_1, NAT_D, MATRIX_1;
schemes ;
registrations STRUCT_0, INT_1, RELSET_1, VECTSP_1, FINSEQ_2, XXREAL_0, FUNCOP_1, XREAL_0, XBOOLE_0, FUNCT_1, ORDINAL1, MATRIX_0, MATRIX_6;
constructors HIDDEN, REAL_1, MATRIX_6, MATRIX13, POLYNOM1, FVSUM_1, MATRIX_0, MATRIX_1, MATRIX_4;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities MATRIX_0, MATRIX_3, FVSUM_1, MATRIX_4, FINSEQ_1, FINSEQ_2, ALGSTR_0, MATRIX_1;
expansions ;
Lm1:
for n being Element of NAT
for k being Nat st k <= n & k >= 1 holds
(k - 1) mod n = k - 1
Lm2:
for n, i, j being Nat st i in Seg n & j in Seg n holds
((j - i) mod n) + 1 in Seg n
Lm3:
for n, i, j being Nat st ( [i,j] in [:(Seg n),(Seg n):] or [j,i] in [:(Seg n),(Seg n):] ) holds
((j - i) mod n) + 1 in Seg n