environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, CARD_3, FUNCT_1, RELAT_1, FINSEQ_1, XBOOLE_0, ARYTM_3, ARYTM_1, XXREAL_0, CARD_1, TARSKI, NAT_1, ZFMISC_1, ORDINAL4, PROB_1, FINSUB_1, SETFAM_1, PROB_2, MEASURE9, MSSUBFAM, FUNCOP_1, SUPINF_2, VALUED_0, PARTFUN1, MEASURE1, ORDINAL2, SERIES_1, MESFUNC5, SUPINF_1, MEASURE4, SEQ_2, MATRIX_1, QC_LANG1, MATRIXC1, ORDINAL1, PRE_POLY, TREES_1, FINSEQ_3, INCSP_1, FINSEQ_2, XREAL_0, MEASURE8, REAL_1, XCMPLX_0, COMPLEX1, DBLSEQ_1, DBLSEQ_2, MESFUNC9, RFINSEQ, SIMPLEX0, ASYMPT_1, SRINGS_3, DBLSEQ_3, LATTICE5;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSUB_1, CARD_3, NUMBERS, XXREAL_3, BINOP_1, XTUPLE_0, PROB_1, XCMPLX_0, XREAL_0, XXREAL_0, SIMPLEX0, NAT_1, VALUED_0, SUPINF_1, SEQ_1, MEASURE8, FINSEQ_1, FINSEQ_2, FINSEQOP, SUPINF_2, PROB_2, MEASURE1, MEASURE4, MESFUNC1, MESFUNC5, MESFUNC9, MATRIX_0, SEQ_2, SERIES_1, RVSUM_1, RFINSEQ, WSIERP_1, MATRLIN, EXTREAL1, SRINGS_3, DBLSEQ_3;
definitions ;
theorems TARSKI, XBOOLE_0, XREAL_0, FINSEQ_1, NAT_1, FUNCT_1, CARD_3, XXREAL_0, ZFMISC_1, FINSEQ_3, XBOOLE_1, PROB_2, XREAL_1, PROB_1, FINSUB_1, SETFAM_1, FUNCOP_1, XXREAL_3, MEASURE1, VALUED_0, FUNCT_2, MEASURE7, RELAT_1, MESFUNC5, EXTREAL1, MESFUNC9, FINSEQ_2, PARTFUN1, ORDINAL1, RINFSUP2, MEASURE8, MESFUNC3, RFINSEQ, PRE_POLY, MATRLIN, RVSUM_1, MESFUNC1, MATRPROB, ORDERS_1, SERIES_1, SUPINF_2, VALUED_1, MATRIX_0, ROUGHS_1, FINSEQOP, SEQM_3, POLYNOM3, XTUPLE_0, SRINGS_3, SEQ_1, DBLSEQ_3;
schemes FINSEQ_1, NAT_1, FUNCT_2, MATRIX_0, FINSEQ_2, BINOP_1;
registrations XREAL_0, MEMBERED, FUNCT_1, XBOOLE_0, FINSEQ_1, RELAT_1, SUBSET_1, XXREAL_0, ROUGHS_1, NUMBERS, VALUED_0, FUNCT_2, ORDINAL1, RELSET_1, FINSUB_1, MEASURE1, MESFUNC5, MATRLIN, NAT_1, XXREAL_3, CARD_1, PBOOLE, SIMPLEX0, SEQ_2, SEQ_1, SETFAM_1, NUMPOLY1, SRINGS_3, DBLSEQ_3;
constructors HIDDEN, PROB_2, EXTREAL1, SUPINF_1, MESFUNC9, RINFSUP2, FINSEQOP, MATRPROB, MATRLIN, MEASURE6, SEQ_1, MEASURE8, SERIES_1, WSIERP_1, COMSEQ_2, RFINSEQ, SRINGS_3, DBLSEQ_3;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities FINSEQ_1, XXREAL_3, BINOP_1, SRINGS_3;
expansions FINSEQ_1, SETFAM_1, PARTFUN1;
RFINSEQlm3:
for n being Nat
for D being set
for f being FinSequence of D st len f <= n holds
f | n = f
RFINSEQ6:
for D being set
for f being FinSequence of D
for n, m being Nat st n in dom f & m in Seg n holds
( (f | n) . m = f . m & m in dom f )
RFINSEQ8:
for D being set
for f being FinSequence of D
for n being Nat holds (f | n) ^ (f /^ n) = f
LM:
for X being set
for P being non empty Subset-Family of X holds
( P --> 0. is V224() & P --> 0. is additive & P --> 0. is zeroed )
LL1:
( <*+infty*> is nonnegative & <*+infty*> is V251() )
LL2:
( <*-infty*> is nonpositive & <*-infty*> is V252() )