let y be Real; :: thesis:
let A be closed-interval Subset of REAL ; :: thesis:
let f be Function of A,REAL ; :: thesis:
assume A1: vol A <> 0 ; :: thesis:
assume y in rng (lower_sum_set f) ; :: thesis:
then consider D3 being Element of divs A such that
A2: ( D3 in dom (lower_sum_set f) & y = (lower_sum_set f) . D3 ) by PARTFUN1:26;
reconsider D3 = D3 as Division of A by INTEGRA1:def 3;
A3: len D3 in Seg (len D3) by FINSEQ_1:5;
rng D3 <> {} ;
then A5: 1 in dom D3 by FINSEQ_3:34;

per cases ;

suppose A6: D3 . 1 <> lower_bound A ; :: thesis:

D3 . 1 in A by A5, INTEGRA1:8;
then lower_bound A <= D3 . 1 by INTEGRA2:1;
then D3 . 1 > lower_bound A by A6, XXREAL_0:1;
hence ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) by A2; :: thesis:

end;

suppose A7: D3 . 1 = lower_bound A ; :: thesis:

A8: D3 . (len D3) = upper_bound A by INTEGRA1:def 2;
A9: len D3 in dom D3 by A3, FINSEQ_1:def 3;
vol A >= 0 by INTEGRA1:11;
then (upper_bound A) - (lower_bound A) > 0 by A1, INTEGRA1:def 6;
then A10: upper_bound A > lower_bound A by XREAL_1:49;
then A11: len D3 > 1 by A5, A7, A8, A9, GOBOARD2:18;
then reconsider D = D3 /^ 1 as increasing FinSequence of REAL by INTEGRA1:36;
A12: ( len D = (len D3) - 1 & ( for m being Element of NAT st m in dom D holds
D . m = D3 . (m + 1) ) ) by A11, RFINSEQ:def 2;
then len D <> 0 by A7, A10, INTEGRA1:def 2;
then reconsider D = D as non empty increasing FinSequence of REAL ;
( rng D c= rng D3 & rng D3 c= A ) by FINSEQ_5:36, INTEGRA1:def 2;
then A13: rng D c= A by XBOOLE_1:1;
A14: (len D) + 1 = len D3 by A12;
len D in dom D by FINSEQ_5:6;
then D . (len D) = upper_bound A by A8, A11, A14, RFINSEQ:def 2;
then reconsider D = D as Division of A by A13, INTEGRA1:def 2;
D in divs A by INTEGRA1:def 3;
then A15: D in dom (lower_sum_set f) by INTEGRA1:def 12;
A16: y = (lower_sum_set f) . D

A17: y = lower_sum f,D3 by A2, INTEGRA1:def 12
.= Sum (lower_volume f,D3) by INTEGRA1:def 10
.= Sum (((lower_volume f,D3) | 1) ^ ((lower_volume f,D3) /^ 1)) by RFINSEQ:21 ;
A18: (lower_volume f,D3) | 1 = <*((lower_volume f,D3) . 1)*>

A19: 1 <= len (lower_volume f,D3) by A11, INTEGRA1:def 8;
then A20: len ((lower_volume f,D3) | 1) = 1 by FINSEQ_1:80;
A21: 1 in dom (lower_volume f,D3) by A19, FINSEQ_3:27;
1 in Seg 1 by FINSEQ_1:3;
then ((lower_volume f,D3) | 1) . 1 = (lower_volume f,D3) . 1 by A21, RFINSEQ:19;
hence (lower_volume f,D3) | 1 = <*((lower_volume f,D3) . 1)*> by A20, FINSEQ_1:57; :: thesis:

end;

A22: vol (divset D3,1) = (upper_bound (divset D3,1)) - (lower_bound (divset D3,1)) by INTEGRA1:def 6
.= (upper_bound (divset D3,1)) - (lower_bound A) by A5, INTEGRA1:def 5
.= (D3 . 1) - (lower_bound A) by A5, INTEGRA1:def 5
.= 0 by A7 ;
A23: (lower_volume f,D3) . 1 = (lower_bound (rng (f | (divset D3,1)))) * (vol (divset D3,1)) by A5, INTEGRA1:def 8;
(lower_volume f,D3) /^ 1 = lower_volume f,D

A24: 2 -' 1 = 2 - 1 by XREAL_1:235
.= 1 ;
A25: len D3 >= 1 + 1 by A11, NAT_1:13;
then len (lower_volume f,D3) >= 2 by INTEGRA1:def 8;
then A26: mid (lower_volume f,D3),2,(len (lower_volume f,D3)) = (lower_volume f,D3) /^ 1 by A24, JORDAN3:26;
A27: ( 2 <= len (lower_volume f,D3) & 1 <= len (lower_volume f,D3) ) by A11, A25, INTEGRA1:def 8;
A28: len (mid (lower_volume f,D3),2,(len (lower_volume f,D3))) = len (lower_volume f,D)

len (mid (lower_volume f,D3),2,(len (lower_volume f,D3))) = ((len (lower_volume f,D3)) -' 2) + 1 by A27, JORDAN3:27
.= ((len D3) -' 2) + 1 by INTEGRA1:def 8
.= ((len D3) - 2) + 1 by A25, XREAL_1:235
.= (len D3) - 1 ;
hence len (mid (lower_volume f,D3),2,(len (lower_volume f,D3))) = len (lower_volume f,D) by A12, INTEGRA1:def 8; :: thesis:

end;

let i be Nat; :: thesis:
A29: i in NAT by ORDINAL1:def 13;
assume A30: ( 1 <= i & i <= len (mid (lower_volume f,D3),2,(len (lower_volume f,D3))) ) ; :: thesis:
then A31: ( 1 <= i & i <= len D ) by A28, INTEGRA1:def 8;
then ( 1 <= i & i <= (len (lower_volume f,D3)) - 1 ) by A12, INTEGRA1:def 8;
then ( 1 <= i & i <= ((len (lower_volume f,D3)) - 2) + 1 ) ;
then A32: (mid (lower_volume f,D3),2,(len (lower_volume f,D3))) . i = (lower_volume f,D3) . ((i + 2) - 1) by A27, A29, JORDAN3:31
.= (lower_volume f,D3) . (i + 1) ;
( 1 <= i + 1 & i + 1 <= len D3 ) by A12, A31, NAT_1:12, XREAL_1:21;
then A33: i + 1 in Seg (len D3) by FINSEQ_1:3;
then i + 1 in dom D3 by FINSEQ_1:def 3;
then A34: (mid (lower_volume f,D3),2,(len (lower_volume f,D3))) . i = (lower_bound (rng (f | (divset D3,(i + 1))))) * (vol (divset D3,(i + 1))) by A32, INTEGRA1:def 8;
A35: divset D3,(i + 1) = divset D,i

A36: 1 <> i + 1 by A30, NAT_1:13;
i + 1 in dom D3 by A33, FINSEQ_1:def 3;
then A37: ( upper_bound (divset D3,(i + 1)) = D3 . (i + 1) & lower_bound (divset D3,(i + 1)) = D3 . ((i + 1) - 1) ) by A36, INTEGRA1:def 5;
A38: i in dom D by A31, FINSEQ_3:27;
then A39: D . i = D3 . (i + 1) by A11, RFINSEQ:def 2;

per cases ;

suppose A40: i = 1 ; :: thesis:

then A41: ( lower_bound (divset D,i) = lower_bound A & upper_bound (divset D,i) = D . i ) by A38, INTEGRA1:def 5;
divset D3,(i + 1) = [.(lower_bound A),(D . i).] by A7, A37, A39, A40, INTEGRA1:5;
hence divset D3,(i + 1) = divset D,i by A41, INTEGRA1:5; :: thesis:

end;

suppose A42: i <> 1 ; :: thesis:

then A43: ( lower_bound (divset D,i) = D . (i - 1) & upper_bound (divset D,i) = D . i ) by A38, INTEGRA1:def 5;
( i - 1 in dom D & i - 1 in NAT ) by A38, A42, INTEGRA1:9;
then ( i - 1 in dom D & i - 1 is Nat ) ;
then D . (i - 1) = D3 . ((i - 1) + 1) by A11, RFINSEQ:def 2
.= D3 . i ;
then divset D3,(i + 1) = [.(lower_bound (divset D,i)),(upper_bound (divset D,i)).] by A37, A39, A43, INTEGRA1:5;
hence divset D3,(i + 1) = divset D,i by INTEGRA1:5; :: thesis:

end;

i in Seg (len D) by A31, FINSEQ_1:3;
then i in dom D by FINSEQ_1:def 3;
hence (mid (lower_volume f,D3),2,(len (lower_volume f,D3))) . i = (lower_volume f,D) . i by A34, A35, INTEGRA1:def 8; :: thesis:

end;

hence (lower_volume f,D3) /^ 1 = lower_volume f,D by A26, A28, FINSEQ_1:18; :: thesis:

end;

then y = 0 + (Sum (lower_volume f,D)) by A17, A18, A22, A23, RVSUM_1:106
.= lower_sum f,D by INTEGRA1:def 10 ;
hence y = (lower_sum_set f) . D by A15, INTEGRA1:def 12; :: thesis:

end;

rng D <> {} ;
then 1 in dom D by FINSEQ_3:34;
then A44: D . 1 = D3 . (1 + 1) by A11, RFINSEQ:def 2
.= D3 . 2 ;
1 + 1 <= len D3 by A11, NAT_1:13;
then 2 in dom D3 by FINSEQ_3:27;
then D3 . 1 < D3 . 2 by A5, SEQM_3:def 1;
hence ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) by A7, A15, A16, A44; :: thesis:

end;

hence ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) ; :: thesis:

end;

hence ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) ; :: thesis: