environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, FINSEQ_1, INTEGRA1, SEQ_4, XXREAL_0, XXREAL_1, VALUED_0, RELAT_1, ARYTM_3, FUNCT_1, CARD_1, NAT_1, CLASSES1, FINSEQ_5, ARYTM_1, ORDINAL4, XBOOLE_0, JORDAN3, MEMBERED, MEMBER_1, TARSKI, PARTFUN1, XXREAL_2, VALUED_1, MEASURE7, CARD_3, SEQ_1, INTEGRA2, MEASURE5, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0, XREAL_0, XXREAL_2, XXREAL_3, MEMBERED, MEMBER_1, XCMPLX_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, RFUNCT_1, RVSUM_1, INTEGRA1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, FINSEQ_6, RCOMP_1, FINSEQ_5, CLASSES1, RFINSEQ, MEASURE5, MEASURE6;
definitions TARSKI, XBOOLE_0, XXREAL_2;
theorems SEQ_4, SUBSET_1, PARTFUN1, INTEGRA1, RFUNCT_1, FUNCT_1, FINSEQ_1, RVSUM_1, NEWTON, RCOMP_1, NAT_1, RFINSEQ, CARD_1, FINSEQ_5, FINSEQ_3, RELAT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, MEMBERED, VALUED_1, XXREAL_2, TARSKI, SEQM_3, CLASSES1, FINSEQ_6, MEMBER_1, XXREAL_3, VALUED_0;
schemes SUBSET_1, SEQ_1, NAT_1;
registrations RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, FINSEQ_1, INTEGRA1, VALUED_0, VALUED_1, XXREAL_2, CARD_1, SEQ_2, RELSET_1, XXREAL_3, MEMBER_1, MEASURE5, NAT_1;
constructors HIDDEN, PARTFUN1, REAL_1, NAT_1, SEQM_3, VALUED_0, RFUNCT_1, RFINSEQ, BINARITH, FINSEQ_5, FINSEQ_6, INTEGRA1, XXREAL_2, NAT_D, RVSUM_1, SEQ_4, CLASSES1, RELSET_1, SEQ_2, MEMBER_1, MEASURE6, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, VALUED_1, RELAT_1;
expansions TARSKI, XBOOLE_0, XXREAL_2;
LM:
for p being FinSequence of REAL st ( for n being Nat st n in dom p & n + 1 in dom p holds
p . n <= p . (n + 1) ) holds
for i, j being Nat st i in dom p & j in dom p & i <= j holds
p . i <= p . j