let I be non empty closed_interval Subset of REAL; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: verum