environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, COMSEQ_1, PARTFUN1, REAL_1, ORDINAL2, NAT_1, SEQ_1, FCONT_1, RELAT_1, TARSKI, SEQ_2, FUNCT_2, ARYTM_1, FUNCT_1, ARYTM_3, VALUED_1, COMPLEX1, XBOOLE_0, ORDINAL4, VALUED_0, CARD_1, XXREAL_0, XREAL_0, RCOMP_1, CFCONT_1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, PARTFUN1, FUNCT_2, SEQ_1, RELSET_1, VALUED_0, VALUED_1, CFUNCT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, XXREAL_0, RECDEF_1;
definitions TARSKI, COMSEQ_2;
theorems TARSKI, NAT_1, FUNCT_1, COMPLEX1, SEQ_1, SEQM_3, SEQ_4, COMSEQ_1, COMSEQ_2, COMSEQ_3, PARTFUN1, CFUNCT_1, RELAT_1, FUNCT_2, PARTFUN2, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, VALUED_1, VALUED_0, XCMPLX_0;
schemes NAT_1, RECDEF_1, FUNCT_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, NAT_1, MEMBERED, VALUED_0, VALUED_1, COMSEQ_2, XCMPLX_0;
constructors HIDDEN, PARTFUN1, XXREAL_0, REAL_1, NAT_1, COMSEQ_2, CFUNCT_1, COMSEQ_3, RECDEF_1, SEQM_3, VALUED_1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities VALUED_1;
expansions TARSKI, COMSEQ_2;
theorem Th1:
for
seq1,
seq2,
seq3 being
Complex_Sequence holds
(
seq1 = seq2 - seq3 iff for
n being
Nat holds
seq1 . n = (seq2 . n) - (seq3 . n) )
:: COMPLEX SEQUENCE
::