let A be closed-interval Subset of REAL ; :: thesis:
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:
( 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:
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:26;
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: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 A3, A4, 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;

(divs A) /\ (dom (upper_sum_set (chi A,A))) = (divs A) /\ (divs A) by INTEGRA1:def 11;
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:
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
assume D1 in (divs A) /\ (dom (upper_sum_set (chi A,A))) ; :: thesis:
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 8
.= upper_sum (chi A,A),D2 by A7, 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
A8: rng ((upper_sum_set (chi A,A)) | (divs A)) = {x} by A5, PARTFUN2:56;
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:
( 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:
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:26;
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: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 A11, A12, 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 A13: chi A,A is upper_integrable by A8, INTEGRA1:def 13;
vol A in rng (upper_sum_set (chi A,A))

proof

consider D1 being Element of divs A;
D1 in divs A ;
then A14: D1 in dom (upper_sum_set (chi A,A)) by INTEGRA1:def 11;
then A15: (upper_sum_set (chi A,A)) . D1 in rng (upper_sum_set (chi A,A)) by FUNCT_1:def 5;
A16: (upper_sum_set (chi A,A)) . D1 = (upper_sum_set (chi A,A)) /. D1 by A14, PARTFUN1:def 8;
D1 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:

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:99;
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:22;
then A18: 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 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:
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
assume D1 in (divs A) /\ (dom (lower_sum_set (chi A,A))) ; :: thesis:
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 8
.= lower_sum (chi A,A),D2 by A21, 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
A22: rng ((lower_sum_set (chi A,A)) | (divs A)) = {x} by A19, PARTFUN2:56;
vol A in rng (lower_sum_set (chi A,A))

proof

consider D1 being Element of divs A;
D1 in divs A ;
then A23: D1 in dom (lower_sum_set (chi A,A)) by INTEGRA1:def 12;
then A24: (lower_sum_set (chi A,A)) . D1 in rng (lower_sum_set (chi A,A)) by FUNCT_1:def 5;
A25: (lower_sum_set (chi A,A)) . D1 = (lower_sum_set (chi A,A)) /. D1 by A23, PARTFUN1:def 8;
D1 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:

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:99;
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:22;
then A27: lower_integral (chi A,A) = vol A by INTEGRA1:def 16;
chi A,A is lower_integrable by A22, A1, INTEGRA1:def 14;
hence ( chi A,A is integrable & integral (chi A,A) = vol A ) by A13, A18, A27, INTEGRA1:def 17, INTEGRA1:def 18; :: thesis: