environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, RELAT_1, TARSKI, VALUED_0, ORDINAL1, RFINSEQ, XXREAL_0, ARYTM_1, SUBSET_1, FUNCT_1, ARYTM_3, INT_1, ORDINAL4, XBOOLE_0, NAT_1, VALUED_1, CARD_3, BINOP_2, SETWISEO, BINOP_1, SETWOP_2, CARD_1, FINSOP_1, PARTFUN1, COMPLEX1, INT_2, PARTFUN3, INT_6, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, INT_1, INT_2, ORDINAL1, NUMBERS, RELAT_1, PARTFUN1, PARTFUN3, XXREAL_0, XREAL_0, FUNCT_1, VALUED_0, VALUED_1, BINOP_2, SETWISEO, RFINSEQ, BINOP_1, FINSEQ_1, SETWOP_2, RVSUM_1, XCMPLX_0, NAT_1, FINSOP_1;
definitions INT_2, FUNCT_1;
theorems INT_1, FUNCT_1, FINSEQ_1, RVSUM_1, NAT_1, SETWOP_2, FINSEQ_3, BINOP_2, SETWISEO, TARSKI, NAT_D, INT_2, XCMPLX_0, XCMPLX_1, XREAL_1, RFINSEQ, FINSEQ_5, FINSEQ_2, ABSVALUE, PARTFUN3, XBOOLE_0, XXREAL_0, ORDINAL1, XBOOLE_1, PARTFUN1, XREAL_0, WSIERP_1, VALUED_1, COMPLEX1, RELAT_1;
schemes FINSEQ_1, NAT_1, INT_1;
registrations NUMBERS, XREAL_0, NAT_1, INT_1, RELAT_1, FINSEQ_1, RVSUM_1, XBOOLE_0, MEMBERED, BINOP_2, ORDINAL1, XXREAL_0, VALUED_0, VALUED_1, FUNCT_1, CARD_1;
constructors HIDDEN, FINSOP_1, RFINSEQ, INT_2, BINOP_2, REAL_1, SETWISEO, SETWOP_2, PARTFUN3, XXREAL_0, RVSUM_1, BINOP_1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XCMPLX_0, FINSEQ_1, ORDINAL1;
expansions INT_2, FINSEQ_1, FUNCT_1;
Lm1:
for f being INT -valued FinSequence holds f is FinSequence of INT
Lm2:
for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 + m2) = len m1
Lm3:
for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 - m2) = len m1
Lm4:
for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 (#) m2) = len m1
Lm5:
for z being INT -valued FinSequence holds z is FinSequence of REAL
Lm6:
for m being INT -valued FinSequence
for i, j being Nat st i in dom m & j in dom m & j <> i & m . j <> 0 holds
ex z being Integer st z * (m . i) = (Product m) / (m . j)
Lm7:
for u being object st u in {1} holds
u in INT
by INT_1:def 1;
Lm8:
for m being CR_Sequence holds Product m > 0
Lm9:
for u being INT -valued FinSequence
for m being CR_Sequence
for z1, z2 being Integer st 0 <= z1 & z1 < Product m & ( for i being Nat st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being Nat st i in dom m holds
z2,u . i are_congruent_mod m . i ) holds
z1 = z2
Lm10:
for u, v being Integer
for m being CR_Sequence
for i being Nat st i in dom m holds
((mod (u,m)) - (mod (v,m))) . i,u - v are_congruent_mod m . i