let I be non empty closed_interval Subset of REAL; for f being Function of I,REAL
for D, D1 being Division of I st D . 1 = lower_bound I & D1 = D /^ 1 holds
( upper_sum (f,D1) = upper_sum (f,D) & lower_sum (f,D1) = lower_sum (f,D) )
let f be Function of I,REAL; for D, D1 being Division of I st D . 1 = lower_bound I & D1 = D /^ 1 holds
( upper_sum (f,D1) = upper_sum (f,D) & lower_sum (f,D1) = lower_sum (f,D) )
let D, D1 be Division of I; ( D . 1 = lower_bound I & D1 = D /^ 1 implies ( upper_sum (f,D1) = upper_sum (f,D) & lower_sum (f,D1) = lower_sum (f,D) ) )
assume that
A1:
D . 1 = lower_bound I
and
A2:
D1 = D /^ 1
; ( upper_sum (f,D1) = upper_sum (f,D) & lower_sum (f,D1) = lower_sum (f,D) )
D = <*(D /. 1)*> ^ (D /^ 1)
by FINSEQ_5:29;
then A4:
D = <*(D . 1)*> ^ (D /^ 1)
by FINSEQ_5:6, PARTFUN1:def 6;
A5:
(upper_volume (f,D)) . 1 = 0
proof
divset (
D,1)
= [.(D . 1),(D . 1).]
by A1, COUSIN:50;
then
(
lower_bound (divset (D,1)) = D . 1 &
upper_bound (divset (D,1)) = D . 1 )
by JORDAN5A:19;
then A6:
vol (divset (D,1)) =
(D . 1) - (D . 1)
by INTEGRA1:def 5
.=
0
;
1
in dom D
by FINSEQ_5:6;
then (upper_volume (f,D)) . 1 =
(upper_bound (rng (f | (divset (D,1))))) * (vol (divset (D,1)))
by INTEGRA1:def 6
.=
0
by A6
;
hence
(upper_volume (f,D)) . 1
= 0
;
verum
end;
0 < len (upper_volume (f,D))
;
then Sum (upper_volume (f,D)) =
((upper_volume (f,D)) . 1) + (Sum ((upper_volume (f,D)) /^ 1))
by IRRAT_1:17
.=
Sum (upper_volume (f,D1))
by A4, A1, A2, INTEGRA3:13, A5
.=
upper_sum (f,D1)
by INTEGRA1:def 8
;
hence
upper_sum (f,D1) = upper_sum (f,D)
by INTEGRA1:def 8; lower_sum (f,D1) = lower_sum (f,D)
A7:
(lower_volume (f,D)) . 1 = 0
proof
divset (
D,1)
= [.(D . 1),(D . 1).]
by A1, COUSIN:50;
then
(
lower_bound (divset (D,1)) = D . 1 &
upper_bound (divset (D,1)) = D . 1 )
by JORDAN5A:19;
then A8:
vol (divset (D,1)) =
(D . 1) - (D . 1)
by INTEGRA1:def 5
.=
0
;
1
in dom D
by FINSEQ_5:6;
then (lower_volume (f,D)) . 1 =
(lower_bound (rng (f | (divset (D,1))))) * (vol (divset (D,1)))
by INTEGRA1:def 7
.=
0
by A8
;
hence
(lower_volume (f,D)) . 1
= 0
;
verum
end;
0 < len (lower_volume (f,D))
;
then Sum (lower_volume (f,D)) =
((lower_volume (f,D)) . 1) + (Sum ((lower_volume (f,D)) /^ 1))
by IRRAT_1:17
.=
Sum (lower_volume (f,D1))
by A4, A1, A2, INTEGRA3:13, A7
.=
lower_sum (f,D1)
by INTEGRA1:def 9
;
hence
lower_sum (f,D1) = lower_sum (f,D)
by INTEGRA1:def 9; verum