environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, INTEGRA1, FINSEQ_1, ORDINAL4, CARD_3, ARYTM_1, ARYTM_3, BINOP_2, RELAT_1, FUNCT_1, PARTFUN1, XXREAL_0, FINSEQ_2, NAT_1, XBOOLE_0, REALSET1, VALUED_1, TARSKI, XXREAL_2, ORDINAL2, FCONT_2, INTEGRA2, FUNCT_3, SEQ_2, CARD_1, SEQ_1, COMPLEX1, MEASURE7, FDIFF_1, SEQ_4, XXREAL_1, ZFMISC_1, VALUED_0, SEQM_3, RCOMP_1, INTEGRA5, MEASURE5, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1, COMPLEX1, XXREAL_2, ZFMISC_1, FUNCT_1, RELSET_1, FUNCT_2, RCOMP_1, PARTFUN1, MEASURE6, FINSEQ_1, FUNCOP_1, VALUED_1, SEQ_1, RFUNCT_1, FINSEQ_2, COMSEQ_2, SEQ_2, SEQ_4, BINOP_2, REAL_1, NAT_1, FDIFF_1, RVSUM_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, FCONT_1, FCONT_2, RFUNCT_2, XXREAL_0;
definitions XXREAL_2;
theorems SEQ_4, SUBSET_1, PARTFUN1, INTEGRA1, RFUNCT_1, FUNCT_1, FINSEQ_1, RVSUM_1, SEQ_1, SEQ_2, FDIFF_1, ABSVALUE, NAT_1, TARSKI, INTEGRA2, NAT_2, FINSEQ_2, RCOMP_1, FCONT_2, INTEGRA4, FCONT_1, ROLLE, RFUNCT_2, FDIFF_2, RELAT_1, XREAL_0, FUNCT_2, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, VALUED_1, XXREAL_2, XXREAL_1, RELSET_1, INTEGRA3, MEASURE5, INT_1;
schemes FINSEQ_2;
registrations XBOOLE_0, RELAT_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, FINSEQ_1, RCOMP_1, INTEGRA1, VALUED_0, VALUED_1, FUNCT_2, FINSET_1, XXREAL_2, CARD_1, SEQ_2, RELSET_1, MEASURE5, RVSUM_1, ORDINAL1;
constructors HIDDEN, PARTFUN1, REAL_1, NAT_1, BINOP_2, COMPLEX1, RFUNCT_1, RFUNCT_2, FCONT_1, FCONT_2, FDIFF_1, ZFMISC_1, MEASURE6, INTEGRA2, XXREAL_2, RVSUM_1, SEQ_4, RELSET_1, FUNCOP_1, SEQ_2, INTEGRA3, COMSEQ_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities VALUED_1;
expansions XXREAL_2;
Lm1:
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds
f is_integrable_on A
::
deftheorem Def4 defines
integral INTEGRA5:def 4 :
for a, b being Real
for f being PartFunc of REAL,REAL holds
( ( a <= b implies integral (f,a,b) = integral (f,['a,b']) ) & ( not a <= b implies integral (f,a,b) = - (integral (f,['b,a'])) ) );