let A be non empty closed_interval Subset of REAL; :: thesis: ( chi (A,A) is integrable & integral (chi (A,A)) = vol A )
A1: rng (lower_sum_set (chi (A,A))) c= rng ((lower_sum_set (chi (A,A))) | (divs A))

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in rng (lower_sum_set (chi (A,A))) or x1 in rng ((lower_sum_set (chi (A,A))) | (divs A)) )
( x1 in rng (lower_sum_set (chi (A,A))) implies x1 in rng ((lower_sum_set (chi (A,A))) | (divs A)) )

proof

assume x1 in rng (lower_sum_set (chi (A,A))) ; :: thesis: x1 in rng ((lower_sum_set (chi (A,A))) | (divs A))
then consider D1 being Element of divs A such that
A2: D1 in dom (lower_sum_set (chi (A,A))) and
A3: (lower_sum_set (chi (A,A))) . D1 = x1 by PARTFUN1:3;
D1 in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) by A2, XBOOLE_1:28;
then A4: D1 in dom ((lower_sum_set (chi (A,A))) | (divs A)) by RELAT_1:61;
then ((lower_sum_set (chi (A,A))) | (divs A)) . D1 = (lower_sum_set (chi (A,A))) . D1 by FUNCT_1:47;
hence x1 in rng ((lower_sum_set (chi (A,A))) | (divs A)) by A3, A4, FUNCT_1:def 3; :: thesis: verum

end;

hence ( not x1 in rng (lower_sum_set (chi (A,A))) or x1 in rng ((lower_sum_set (chi (A,A))) | (divs A)) ) ; :: thesis: verum

end;

(divs A) /\ (dom (upper_sum_set (chi (A,A)))) = (divs A) /\ (divs A) by FUNCT_2:def 1, INTEGRA1:def 10;
then A5: divs A meets dom (upper_sum_set (chi (A,A))) by XBOOLE_0:def 7;
A6: 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 = vol A

proof

let D1 be Element of divs A; :: thesis: ( D1 in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) implies (upper_sum_set (chi (A,A))) /. D1 = vol A )
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
assume D1 in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) ; :: thesis: (upper_sum_set (chi (A,A))) /. D1 = vol A
then A7: D1 in dom (upper_sum_set (chi (A,A))) by XBOOLE_0:def 4;
then (upper_sum_set (chi (A,A))) /. D1 = (upper_sum_set (chi (A,A))) . D1 by PARTFUN1:def 6
.= upper_sum ((chi (A,A)),D2) by A7, FUNCT_2:def 1, INTEGRA1:def 10
.= Sum (upper_volume ((chi (A,A)),D2)) by INTEGRA1:def 8 ;
hence (upper_sum_set (chi (A,A))) /. D1 = vol A by INTEGRA1:24; :: thesis: 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
A8: rng ((upper_sum_set (chi (A,A))) | (divs A)) = {x} by A5, PARTFUN2:37;
A9: rng (upper_sum_set (chi (A,A))) c= rng ((upper_sum_set (chi (A,A))) | (divs A))

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in rng (upper_sum_set (chi (A,A))) or x1 in rng ((upper_sum_set (chi (A,A))) | (divs A)) )
( x1 in rng (upper_sum_set (chi (A,A))) implies x1 in rng ((upper_sum_set (chi (A,A))) | (divs A)) )

proof

assume x1 in rng (upper_sum_set (chi (A,A))) ; :: thesis: x1 in rng ((upper_sum_set (chi (A,A))) | (divs A))
then consider D1 being Element of divs A such that
A10: D1 in dom (upper_sum_set (chi (A,A))) and
A11: (upper_sum_set (chi (A,A))) . D1 = x1 by PARTFUN1:3;
D1 in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) by A10, XBOOLE_1:28;
then A12: D1 in dom ((upper_sum_set (chi (A,A))) | (divs A)) by RELAT_1:61;
then ((upper_sum_set (chi (A,A))) | (divs A)) . D1 = (upper_sum_set (chi (A,A))) . D1 by FUNCT_1:47;
hence x1 in rng ((upper_sum_set (chi (A,A))) | (divs A)) by A11, A12, FUNCT_1:def 3; :: thesis: verum

end;

hence ( not x1 in rng (upper_sum_set (chi (A,A))) or x1 in rng ((upper_sum_set (chi (A,A))) | (divs A)) ) ; :: thesis: verum

end;

then A13: chi (A,A) is upper_integrable by A8, 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 A14: the Element of divs A in dom (upper_sum_set (chi (A,A))) by FUNCT_2:def 1, INTEGRA1:def 10;
then A15: (upper_sum_set (chi (A,A))) . the Element of divs A in rng (upper_sum_set (chi (A,A))) by FUNCT_1:def 3;
A16: (upper_sum_set (chi (A,A))) . the Element of divs A = (upper_sum_set (chi (A,A))) /. the Element of divs A by A14, PARTFUN1:def 6;
the Element of divs A in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) by A14, XBOOLE_0:def 4;
hence vol A in rng (upper_sum_set (chi (A,A))) by A6, A15, A16; :: thesis: verum

end;

then A17: x = vol A by A8, A9, TARSKI:def 1;
rng ((upper_sum_set (chi (A,A))) | (divs A)) c= rng (upper_sum_set (chi (A,A))) by RELAT_1:70;
then rng (upper_sum_set (chi (A,A))) = {x} by A8, A9, XBOOLE_0:def 10;
then lower_bound (rng (upper_sum_set (chi (A,A)))) = vol A by A17, SEQ_4:9;
then A18: 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, INTEGRA1:def 11;
then A19: divs A meets dom (lower_sum_set (chi (A,A))) by XBOOLE_0:def 7;
A20: 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 = vol A

proof

let D1 be Element of divs A; :: thesis: ( D1 in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) implies (lower_sum_set (chi (A,A))) /. D1 = vol A )
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
assume D1 in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) ; :: thesis: (lower_sum_set (chi (A,A))) /. D1 = vol A
then A21: D1 in dom (lower_sum_set (chi (A,A))) by XBOOLE_0:def 4;
then (lower_sum_set (chi (A,A))) /. D1 = (lower_sum_set (chi (A,A))) . D1 by PARTFUN1:def 6
.= lower_sum ((chi (A,A)),D2) by A21, FUNCT_2:def 1, INTEGRA1:def 11
.= Sum (lower_volume ((chi (A,A)),D2)) by INTEGRA1:def 9 ;
hence (lower_sum_set (chi (A,A))) /. D1 = vol A by INTEGRA1:23; :: thesis: 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
A22: rng ((lower_sum_set (chi (A,A))) | (divs A)) = {x} by A19, 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 A23: the Element of divs A in dom (lower_sum_set (chi (A,A))) by FUNCT_2:def 1, INTEGRA1:def 11;
then A24: (lower_sum_set (chi (A,A))) . the Element of divs A in rng (lower_sum_set (chi (A,A))) by FUNCT_1:def 3;
A25: (lower_sum_set (chi (A,A))) . the Element of divs A = (lower_sum_set (chi (A,A))) /. the Element of divs A by A23, PARTFUN1:def 6;
the Element of divs A in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) by A23, XBOOLE_0:def 4;
hence vol A in rng (lower_sum_set (chi (A,A))) by A20, A24, A25; :: thesis: verum

end;

then A26: x = vol A by A22, A1, TARSKI:def 1;
rng ((lower_sum_set (chi (A,A))) | (divs A)) c= rng (lower_sum_set (chi (A,A))) by RELAT_1:70;
then rng (lower_sum_set (chi (A,A))) = {x} by A22, A1, XBOOLE_0:def 10;
then upper_bound (rng (lower_sum_set (chi (A,A)))) = vol A by A26, SEQ_4:9;
then A27: lower_integral (chi (A,A)) = vol A by INTEGRA1:def 15;
chi (A,A) is lower_integrable by A22, A1, INTEGRA1:def 13;
hence ( chi (A,A) is integrable & integral (chi (A,A)) = vol A ) by A13, A18, A27, INTEGRA1:def 16, INTEGRA1:def 17; :: thesis: verum