let A be non empty closed_interval Subset of REAL; ( chi (A,A) is integrable & integral (chi (A,A)) = vol A )
(divs A) /\ (dom (upper_sum_set (chi (A,A)))) = (divs A) /\ (divs A)
by FUNCT_2:def 1;
then A1:
divs A meets dom (upper_sum_set (chi (A,A)))
by XBOOLE_0:def 7;
reconsider vA = vol A as Element of REAL by XREAL_0:def 1;
A2:
for D1 being Element of divs A st D1 in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) holds
(upper_sum_set (chi (A,A))) /. D1 = vA
proof
let D1 be
Element of
divs A;
( D1 in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) implies (upper_sum_set (chi (A,A))) /. D1 = vA )
reconsider D2 =
D1 as
Division of
A by INTEGRA1:def 3;
assume
D1 in (divs A) /\ (dom (upper_sum_set (chi (A,A))))
;
(upper_sum_set (chi (A,A))) /. D1 = vA
(upper_sum_set (chi (A,A))) /. D1 =
(upper_sum_set (chi (A,A))) . D1
.=
upper_sum (
(chi (A,A)),
D2)
by INTEGRA1:def 10
.=
Sum (upper_volume ((chi (A,A)),D2))
by INTEGRA1:def 8
;
hence
(upper_sum_set (chi (A,A))) /. D1 = vA
by INTEGRA1:24;
verum
end;
then
(upper_sum_set (chi (A,A))) | (divs A) is constant
by PARTFUN2:35;
then consider x being Element of REAL such that
A3:
rng ((upper_sum_set (chi (A,A))) | (divs A)) = {x}
by A1, PARTFUN2:37;
A4:
chi (A,A) is upper_integrable
by A3, INTEGRA1:def 12;
vol A in rng (upper_sum_set (chi (A,A)))
proof
set D1 = the
Element of
divs A;
the
Element of
divs A in divs A
;
then A5:
the
Element of
divs A in dom (upper_sum_set (chi (A,A)))
by FUNCT_2:def 1;
then A6:
(upper_sum_set (chi (A,A))) . the
Element of
divs A in rng (upper_sum_set (chi (A,A)))
by FUNCT_1:def 3;
A7:
(upper_sum_set (chi (A,A))) . the
Element of
divs A = (upper_sum_set (chi (A,A))) /. the
Element of
divs A
;
the
Element of
divs A in (divs A) /\ (dom (upper_sum_set (chi (A,A))))
by A5, XBOOLE_0:def 4;
hence
vol A in rng (upper_sum_set (chi (A,A)))
by A2, A6, A7;
verum
end;
then A8:
x = vol A
by A3, TARSKI:def 1;
rng (upper_sum_set (chi (A,A))) = {x}
by A3;
then
lower_bound (rng (upper_sum_set (chi (A,A)))) = vol A
by A8, SEQ_4:9;
then A9:
upper_integral (chi (A,A)) = vol A
by INTEGRA1:def 14;
(divs A) /\ (dom (lower_sum_set (chi (A,A)))) = (divs A) /\ (divs A)
by FUNCT_2:def 1;
then A10:
divs A meets dom (lower_sum_set (chi (A,A)))
by XBOOLE_0:def 7;
reconsider vA = vol A as Element of REAL by XREAL_0:def 1;
A11:
for D1 being Element of divs A st D1 in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) holds
(lower_sum_set (chi (A,A))) /. D1 = vA
proof
let D1 be
Element of
divs A;
( D1 in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) implies (lower_sum_set (chi (A,A))) /. D1 = vA )
reconsider D2 =
D1 as
Division of
A by INTEGRA1:def 3;
assume
D1 in (divs A) /\ (dom (lower_sum_set (chi (A,A))))
;
(lower_sum_set (chi (A,A))) /. D1 = vA
(lower_sum_set (chi (A,A))) /. D1 =
(lower_sum_set (chi (A,A))) . D1
.=
lower_sum (
(chi (A,A)),
D2)
by INTEGRA1:def 11
.=
Sum (lower_volume ((chi (A,A)),D2))
by INTEGRA1:def 9
;
hence
(lower_sum_set (chi (A,A))) /. D1 = vA
by INTEGRA1:23;
verum
end;
then
(lower_sum_set (chi (A,A))) | (divs A) is constant
by PARTFUN2:35;
then consider x being Element of REAL such that
A12:
rng ((lower_sum_set (chi (A,A))) | (divs A)) = {x}
by A10, PARTFUN2:37;
vol A in rng (lower_sum_set (chi (A,A)))
proof
set D1 = the
Element of
divs A;
the
Element of
divs A in divs A
;
then A13:
the
Element of
divs A in dom (lower_sum_set (chi (A,A)))
by FUNCT_2:def 1;
then A14:
(lower_sum_set (chi (A,A))) . the
Element of
divs A in rng (lower_sum_set (chi (A,A)))
by FUNCT_1:def 3;
A15:
(lower_sum_set (chi (A,A))) . the
Element of
divs A = (lower_sum_set (chi (A,A))) /. the
Element of
divs A
;
the
Element of
divs A in (divs A) /\ (dom (lower_sum_set (chi (A,A))))
by A13, XBOOLE_0:def 4;
hence
vol A in rng (lower_sum_set (chi (A,A)))
by A11, A14, A15;
verum
end;
then A16:
x = vol A
by A12, TARSKI:def 1;
rng (lower_sum_set (chi (A,A))) = {x}
by A12;
then
upper_bound (rng (lower_sum_set (chi (A,A)))) = vol A
by A16, SEQ_4:9;
then A17:
lower_integral (chi (A,A)) = vol A
by INTEGRA1:def 15;
chi (A,A) is lower_integrable
by A12, INTEGRA1:def 13;
hence
( chi (A,A) is integrable & integral (chi (A,A)) = vol A )
by A4, A9, A17, INTEGRA1:def 16, INTEGRA1:def 17; verum