let A be closed-interval Subset of REAL ; :: thesis:
(divs A) /\ (dom (upper_sum_set (chi A,A))) = (divs A) /\ (divs A) by INTEGRA1:def 11;
then A1: divs A meets dom (upper_sum_set (chi A,A)) by XBOOLE_0:def 7;
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 = vol A

let D1 be Element of divs A; :: thesis:
assume D1 in (divs A) /\ (dom (upper_sum_set (chi A,A))) ; :: thesis:
then A3: D1 in dom (upper_sum_set (chi A,A)) by XBOOLE_0:def 4;
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
(upper_sum_set (chi A,A)) /. D1 = (upper_sum_set (chi A,A)) . D1 by A3, PARTFUN1:def 8
.= upper_sum (chi A,A),D2 by A3, INTEGRA1:def 11
.= Sum (upper_volume (chi A,A),D2) by INTEGRA1:def 9 ;
hence (upper_sum_set (chi A,A)) /. D1 = vol A by INTEGRA1:26; :: thesis:

end;

then (upper_sum_set (chi A,A)) | (divs A) is constant by PARTFUN2:54;
then consider x being Element of REAL such that
A4: rng ((upper_sum_set (chi A,A)) | (divs A)) = {x} by A1, PARTFUN2:56;
A5: rng ((upper_sum_set (chi A,A)) | (divs A)) c= rng (upper_sum_set (chi A,A)) by RELAT_1:99;
A6: rng (upper_sum_set (chi A,A)) c= rng ((upper_sum_set (chi A,A)) | (divs A))

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

assume x1 in rng (upper_sum_set (chi A,A)) ; :: thesis:
then consider D1 being Element of divs A such that
A7: ( D1 in dom (upper_sum_set (chi A,A)) & (upper_sum_set (chi A,A)) . D1 = x1 ) by PARTFUN1:26;
D1 in (divs A) /\ (dom (upper_sum_set (chi A,A))) by A7, XBOOLE_1:28;
then A8: D1 in dom ((upper_sum_set (chi A,A)) | (divs A)) by RELAT_1:90;
then ((upper_sum_set (chi A,A)) | (divs A)) . D1 = (upper_sum_set (chi A,A)) . D1 by FUNCT_1:70;
hence x1 in rng ((upper_sum_set (chi A,A)) | (divs A)) by A7, A8, FUNCT_1:def 5; :: thesis:

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:

end;

then A9: rng (upper_sum_set (chi A,A)) = {x} by A4, A5, XBOOLE_0:def 10;
then rng (upper_sum_set (chi A,A)) is bounded ;
then rng (upper_sum_set (chi A,A)) is bounded_below ;
then A10: chi A,A is upper_integrable by INTEGRA1:def 13;
x = vol A

consider D1 being Element of divs A;
D1 in divs A ;
then A11: D1 in dom (upper_sum_set (chi A,A)) by INTEGRA1:def 11;
then A12: D1 in (divs A) /\ (dom (upper_sum_set (chi A,A))) by XBOOLE_0:def 4;
A13: (upper_sum_set (chi A,A)) . D1 in rng (upper_sum_set (chi A,A)) by A11, FUNCT_1:def 5;
(upper_sum_set (chi A,A)) . D1 = (upper_sum_set (chi A,A)) /. D1 by A11, PARTFUN1:def 8;
hence vol A in rng (upper_sum_set (chi A,A)) by A2, A12, A13; :: thesis:

end;

hence x = vol A by A4, A6, TARSKI:def 1; :: thesis:

end;

then lower_bound (rng (upper_sum_set (chi A,A))) = vol A by A9, SEQ_4:22;
then A14: upper_integral (chi A,A) = vol A by INTEGRA1:def 15;
(divs A) /\ (dom (lower_sum_set (chi A,A))) = (divs A) /\ (divs A) by INTEGRA1:def 12;
then A15: divs A meets dom (lower_sum_set (chi A,A)) by XBOOLE_0:def 7;
A16: 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

let D1 be Element of divs A; :: thesis:
assume D1 in (divs A) /\ (dom (lower_sum_set (chi A,A))) ; :: thesis:
then A17: D1 in dom (lower_sum_set (chi A,A)) by XBOOLE_0:def 4;
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
(lower_sum_set (chi A,A)) /. D1 = (lower_sum_set (chi A,A)) . D1 by A17, PARTFUN1:def 8
.= lower_sum (chi A,A),D2 by A17, INTEGRA1:def 12
.= Sum (lower_volume (chi A,A),D2) by INTEGRA1:def 10 ;
hence (lower_sum_set (chi A,A)) /. D1 = vol A by INTEGRA1:25; :: thesis:

end;

then (lower_sum_set (chi A,A)) | (divs A) is constant by PARTFUN2:54;
then consider x being Element of REAL such that
A18: rng ((lower_sum_set (chi A,A)) | (divs A)) = {x} by A15, PARTFUN2:56;
A19: rng ((lower_sum_set (chi A,A)) | (divs A)) c= rng (lower_sum_set (chi A,A)) by RELAT_1:99;
A20: rng (lower_sum_set (chi A,A)) c= rng ((lower_sum_set (chi A,A)) | (divs A))

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

assume x1 in rng (lower_sum_set (chi A,A)) ; :: thesis:
then consider D1 being Element of divs A such that
A21: ( D1 in dom (lower_sum_set (chi A,A)) & (lower_sum_set (chi A,A)) . D1 = x1 ) by PARTFUN1:26;
D1 in (divs A) /\ (dom (lower_sum_set (chi A,A))) by A21, XBOOLE_1:28;
then A22: D1 in dom ((lower_sum_set (chi A,A)) | (divs A)) by RELAT_1:90;
then ((lower_sum_set (chi A,A)) | (divs A)) . D1 = (lower_sum_set (chi A,A)) . D1 by FUNCT_1:70;
hence x1 in rng ((lower_sum_set (chi A,A)) | (divs A)) by A21, A22, FUNCT_1:def 5; :: thesis:

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:

end;

then A23: rng (lower_sum_set (chi A,A)) = {x} by A18, A19, XBOOLE_0:def 10;
then rng (lower_sum_set (chi A,A)) is bounded ;
then rng (lower_sum_set (chi A,A)) is bounded_above ;
then A24: chi A,A is lower_integrable by INTEGRA1:def 14;
x = vol A

consider D1 being Element of divs A;
D1 in divs A ;
then A25: D1 in dom (lower_sum_set (chi A,A)) by INTEGRA1:def 12;
then A26: D1 in (divs A) /\ (dom (lower_sum_set (chi A,A))) by XBOOLE_0:def 4;
A27: (lower_sum_set (chi A,A)) . D1 in rng (lower_sum_set (chi A,A)) by A25, FUNCT_1:def 5;
(lower_sum_set (chi A,A)) . D1 = (lower_sum_set (chi A,A)) /. D1 by A25, PARTFUN1:def 8;
hence vol A in rng (lower_sum_set (chi A,A)) by A16, A26, A27; :: thesis:

end;

hence x = vol A by A18, A20, TARSKI:def 1; :: thesis:

end;

then upper_bound (rng (lower_sum_set (chi A,A))) = vol A by A23, SEQ_4:22;
then lower_integral (chi A,A) = vol A by INTEGRA1:def 16;
hence ( chi A,A is integrable & integral (chi A,A) = vol A ) by A10, A14, A24, INTEGRA1:def 17, INTEGRA1:def 18; :: thesis: