begin
begin
begin
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;
begin
begin
begin
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
begin