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