environ
vocabularies HIDDEN, FUNCT_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1, TARSKI, VALUED_0, REAL_1, PARTFUN1, FUNCOP_1, CARD_1, XBOOLE_0, ARYTM_3, VALUED_1, ARYTM_1, COMPLEX1, SEQ_1, ASYMPT_1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, VALUED_0, REAL_1, RELAT_1, FUNCT_1, FUNCOP_1, COMPLEX1, NAT_1, RELSET_1, PARTFUN1, FUNCT_2, VALUED_1;
definitions ORDINAL1;
theorems FUNCT_1, TARSKI, ABSVALUE, FUNCT_2, PARTFUN1, RELSET_1, RELAT_1, XREAL_0, ZFMISC_1, XBOOLE_0, XCMPLX_0, XCMPLX_1, COMPLEX1, VALUED_1, FUNCOP_1, ORDINAL1, NUMBERS;
schemes CLASSES1, FUNCT_2, XBOOLE_0;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, FUNCOP_1, XXREAL_0;
constructors HIDDEN, PARTFUN1, FUNCT_2, XXREAL_0, REAL_1, COMPLEX1, VALUED_1, FUNCOP_1, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities VALUED_1;
expansions ;
theorem Th7:
for
seq,
seq1,
seq2 being
Real_Sequence holds
(
seq = seq1 + seq2 iff for
n being
Nat holds
seq . n = (seq1 . n) + (seq2 . n) )
theorem Th8:
for
seq,
seq1,
seq2 being
Real_Sequence holds
(
seq = seq1 (#) seq2 iff for
n being
Nat holds
seq . n = (seq1 . n) * (seq2 . n) )
theorem Th13:
for
seq1,
seq2,
seq3 being
Real_Sequence holds
(seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
theorem
for
seq1,
seq2,
seq3 being
Real_Sequence holds
seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
theorem
for
seq1,
seq2,
seq3 being
Real_Sequence holds
seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
theorem
for
seq1,
seq2,
seq3 being
Real_Sequence holds
seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3
Lm1:
(- 1) " = - 1
;
theorem
for
seq,
seq1,
seq19 being
Real_Sequence holds
(
(seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq &
(seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq )