environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, XREAL_0, SEQ_1, VALUED_0, FUNCT_1, ARYTM_1, ARYTM_3, COMPLEX1, XXREAL_0, CARD_1, RELAT_1, XXREAL_2, NAT_1, ORDINAL2, REAL_1, VALUED_1, SEQ_2, COMSEQ_1, XCMPLX_0, SQUARE_1;
notations HIDDEN, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, VALUED_0, VALUED_1, FUNCOP_1, SEQ_1, XXREAL_0, SQUARE_1, COMSEQ_1, COMSEQ_2;
definitions COMSEQ_2;
theorems SEQ_1, ABSVALUE, NAT_1, XREAL_0, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1, FUNCT_2, VALUED_0, COMSEQ_2, NUMBERS, SQUARE_1, ORDINAL1;
schemes NAT_1;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, NUMBERS, COMSEQ_2, XCMPLX_0, SQUARE_1, NAT_1, SEQ_1;
constructors HIDDEN, XXREAL_0, REAL_1, NAT_1, COMPLEX1, PARTFUN1, VALUED_1, RELSET_1, FUNCOP_1, COMSEQ_2, SQUARE_1, SEQ_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SQUARE_1, COMPLEX1, VALUED_1;
expansions COMSEQ_2;
theorem Th1:
for
r,
g being
Real holds
( (
- g < r &
r < g ) iff
|.r.| < g )
reconsider zz = 0 as Nat ;
:: CONVERGENT REAL SEQUENCES
:: THE LIMIT OF SEQUENCES
::