environ
vocabularies HIDDEN, FINSEQ_1, RCOMP_1, ORDINAL2, ARYTM_1, RELAT_1, FUNCT_1, PARTFUN1, CARD_3, XBOOLE_0, FUNCT_3, ZFMISC_1, XXREAL_0, REAL_1, SUBSET_1, FINSEQ_2, RFINSEQ, JORDAN3, SEQ_4, CARD_1, INTEGRA1, FUNCOP_1, VALUED_0, NUMBERS, MEASURE7, ORDINAL4, XXREAL_1, XXREAL_2, NAT_1, ARYTM_3, TARSKI, MEMBER_1, MEASURE5, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, RELAT_1, FUNCT_1, RELSET_1, VALUED_0, MEMBERED, MEMBER_1, VALUED_1, SEQ_4, XXREAL_2, COMSEQ_2, SEQ_2, RCOMP_1, FINSEQ_2, PARTFUN2, RFUNCT_1, RVSUM_1, RFINSEQ, FINSEQ_6, PARTFUN1, FINSEQ_1, FUNCT_2, MEASURE5, MEASURE6;
definitions TARSKI, XBOOLE_0, XXREAL_2, FUNCT_2;
theorems TARSKI, RCOMP_1, FINSEQ_1, FINSEQ_2, SEQ_4, FUNCT_1, NAT_1, NAT_2, SUBSET_1, PARTFUN1, RFUNCT_1, MEASURE6, RVSUM_1, PARTFUN2, ZFMISC_1, FUNCT_3, FINSEQ_4, RFINSEQ, RELAT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, FUNCOP_1, XREAL_1, XXREAL_0, FINSOP_1, ORDINAL1, XXREAL_1, VALUED_1, FINSEQ_3, XXREAL_2, SEQM_3, NAT_D, FINSEQ_6, MEMBER_1, MEMBERED, CARD_1, MEASURE5, XREAL_0;
schemes FINSEQ_2, NAT_1, FUNCT_2, XFAMILY;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_2, SEQM_3, VALUED_0, VALUED_1, FINSET_1, XXREAL_2, CARD_1, SEQ_2, RELSET_1, MEMBER_1, MEASURE5;
constructors HIDDEN, PARTFUN1, REAL_1, NAT_1, RCOMP_1, FINSOP_1, PARTFUN2, RFUNCT_1, REALSET1, RFINSEQ, BINARITH, FINSEQ_5, SEQM_3, MEASURE6, FINSEQ_6, BINOP_2, XXREAL_2, NAT_D, RVSUM_1, SEQ_4, RELSET_1, SEQ_2, MEMBER_1, XXREAL_3, MEASURE5, COMSEQ_2, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, RVSUM_1;
expansions TARSKI, XBOOLE_0, XXREAL_2;
definition
let A be non
empty closed_interval Subset of
REAL;
let f be
PartFunc of
A,
REAL;
let D be
Division of
A;
existence
ex b1 being FinSequence of REAL st
( len b1 = len D & ( for i being Nat st i in dom D holds
b1 . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) )
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len D & ( for i being Nat st i in dom D holds
b1 . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) & len b2 = len D & ( for i being Nat st i in dom D holds
b2 . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) holds
b1 = b2
existence
ex b1 being FinSequence of REAL st
( len b1 = len D & ( for i being Nat st i in dom D holds
b1 . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) )
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len D & ( for i being Nat st i in dom D holds
b1 . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) & len b2 = len D & ( for i being Nat st i in dom D holds
b2 . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) holds
b1 = b2
end;
definition
let A be non
empty closed_interval Subset of
REAL;
let f be
PartFunc of
A,
REAL;
set S =
divs A;
existence
ex b1 being Function of (divs A),REAL st
for D being Division of A holds b1 . D = upper_sum (f,D)
uniqueness
for b1, b2 being Function of (divs A),REAL st ( for D being Division of A holds b1 . D = upper_sum (f,D) ) & ( for D being Division of A holds b2 . D = upper_sum (f,D) ) holds
b1 = b2
existence
ex b1 being Function of (divs A),REAL st
for D being Division of A holds b1 . D = lower_sum (f,D)
uniqueness
for b1, b2 being Function of (divs A),REAL st ( for D being Division of A holds b1 . D = lower_sum (f,D) ) & ( for D being Division of A holds b2 . D = lower_sum (f,D) ) holds
b1 = b2
end;
Lm1:
for i, j being Element of NAT
for f being FinSequence st i in dom f & j in dom f & i <= j holds
len (mid (f,i,j)) = (j - i) + 1