environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, SEQ_1, PARTFUN1, CARD_1, ARYTM_3, XXREAL_0, ARYTM_1, RELAT_1, TARSKI, XBOOLE_0, VALUED_1, PROB_1, XXREAL_1, VALUED_0, XXREAL_2, FUNCT_1, SEQ_2, ORDINAL2, COMPLEX1, REAL_1, NAT_1, SQUARE_1, SEQM_3, FUNCT_2, ORDINAL4, LIMFUNC1, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, XXREAL_1, COMPLEX1, REAL_1, SQUARE_1, NAT_1, RELSET_1, PARTFUN1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQM_3, PROB_1, FUNCT_3, RFUNCT_1, RECDEF_1;
definitions SEQ_2, MEMBERED;
theorems TARSKI, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, SEQ_4, SQUARE_1, RFUNCT_1, RFUNCT_2, FUNCT_1, FUNCT_2, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, XXREAL_1, VALUED_1, VALUED_0, NUMBERS;
schemes SEQ_1, FUNCT_2;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, XXREAL_1, VALUED_0, VALUED_1, FUNCT_2, SEQ_2, SEQ_4, SQUARE_1, NAT_1, SEQ_1, FUNCT_1;
constructors HIDDEN, PARTFUN1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1, SEQ_2, SEQM_3, PROB_1, RCOMP_1, RFUNCT_1, RFUNCT_2, RECDEF_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SQUARE_1, XBOOLE_0, PROB_1, VALUED_1;
expansions SEQ_2, MEMBERED;
Lm1:
for r, r1, g being Real st 0 < g & r <= r1 holds
( r - g < r1 & r < r1 + g )
Lm2:
for seq being Real_Sequence
for f1, f2 being PartFunc of REAL,REAL st rng seq c= dom (f1 + f2) holds
( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 )
Lm3:
for seq being Real_Sequence
for f1, f2 being PartFunc of REAL,REAL st rng seq c= dom (f1 (#) f2) holds
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 )
Lm4:
0 in REAL
by XREAL_0:def 1;
reconsider jj = 1 as Real ;
reconsider s1 = id NAT as Real_Sequence by FUNCT_2:7, NUMBERS:19;
Lm5:
for n being Nat holds s1 . n = n
by ORDINAL1:def 12, FUNCT_1:18;