environ
vocabularies HIDDEN, NUMBERS, SEQ_1, COMSEQ_1, SUBSET_1, REAL_1, COMPLEX1, CARD_1, ARYTM_3, RELAT_1, XCMPLX_0, FUNCT_1, SERIES_1, XXREAL_0, ARYTM_1, FUNCOP_1, SEQ_2, VALUED_0, ORDINAL2, NAT_1, PREPOWER, NEWTON, SQUARE_1, VALUED_1, CARD_3, POWER, XXREAL_2, PARTFUN1, TARSKI, FUNCT_7, ASYMPT_1;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, COMPLEX1, REAL_1, NEWTON, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, VALUED_1, SEQ_1, SEQ_2, NAT_1, VALUED_0, SERIES_1, SQUARE_1, POWER, COMSEQ_1, COMSEQ_2;
definitions COMSEQ_2, SERIES_1, VALUED_0;
theorems NAT_1, ABSVALUE, SEQ_1, SEQ_2, SERIES_1, SEQM_3, SEQ_4, POWER, COMPLEX1, COMSEQ_2, SQUARE_1, FUNCT_2, XCMPLX_0, XCMPLX_1, FUNCOP_1, XREAL_1, NEWTON, XXREAL_0, ORDINAL1, VALUED_0, VALUED_1, FUNCT_1, RELAT_1, RELSET_1, PARTFUN1;
schemes NAT_1, SEQ_1, COMSEQ_1, FUNCT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED, COMSEQ_2, NEWTON, VALUED_0, VALUED_1, SEQ_4, SERIES_1, SQUARE_1, SEQ_1, SEQ_2;
constructors HIDDEN, PARTFUN1, FUNCT_3, FUNCOP_1, ARYTM_0, REAL_1, SQUARE_1, NAT_1, SEQM_3, COMSEQ_2, NEWTON, SERIES_1, RECDEF_1, SEQ_2, VALUED_1, SEQ_4, RELSET_1, BINOP_2, RVSUM_1, SEQ_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SERIES_1, SQUARE_1, VALUED_1;
expansions COMSEQ_2, SERIES_1, FUNCT_2;
Lm1:
0c = 0 + (0 * <i>)
;
set C = seq_const 0;
Lm2:
for n being Nat holds (seq_const 0) . n = 0
by SEQ_1:57;
Lm3:
for seq being Complex_Sequence
for n being Nat holds
( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n )
set D = NAT --> 0c;