environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, XREAL_0, ORDINAL1, SEQ_1, ARYTM_3, CARD_1, FUNCT_1, POWER, SEQ_2, ORDINAL2, ARYTM_1, XXREAL_0, COMPLEX1, RELAT_1, INT_1, NAT_1, REAL_1, CARD_3, VALUED_1, VALUED_0, XXREAL_2, PREPOWER, NEWTON, SERIES_1, ABIAN, MEMBERED, XBOOLE_0, IDEAL_1, PBOOLE, TARSKI, FUNCT_7, ASYMPT_1;
notations HIDDEN, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, INT_1, NAT_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, PBOOLE, FUNCT_2, NEWTON, ABIAN, PREPOWER, POWER, FUNCOP_1, XXREAL_0;
definitions PBOOLE, VALUED_0;
theorems SEQ_1, SEQ_2, SEQM_3, SEQ_4, NAT_1, RFUNCT_2, ABSVALUE, INT_1, PREPOWER, POWER, FUNCT_2, NEWTON, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, VALUED_0, VALUED_1, MEMBERED, XCMPLX_0, RELSET_1, PARTFUN1, XREAL_0, TARSKI;
schemes NAT_1, SEQ_1, FUNCT_2, RECDEF_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, POWER, SEQ_2, SEQ_4, XCMPLX_0, SEQ_1;
constructors HIDDEN, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, SEQ_2, SEQM_3, NEWTON, PREPOWER, POWER, PARTFUN1, VALUED_1, SEQ_4, RELSET_1, ABIAN, BINOP_2, COMSEQ_2, SEQ_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
equalities VALUED_1, XCMPLX_0;
expansions VALUED_1, PBOOLE, VALUED_0;
Lm1:
for seq, seq1, seq2 being complex-valued ManySortedSet of NAT holds
( seq = seq1 + seq2 iff for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) )
reconsider jj = 1 as Real ;
Lm2:
1 in REAL
by XREAL_0:def 1;