let y be Real; :: thesis: for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL st vol A <> 0 & y in rng (lower_sum_set f) holds

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 )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st vol A <> 0 & y in rng (lower_sum_set f) holds

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 )

let f be Function of A,REAL; :: thesis: ( vol A <> 0 & y in rng (lower_sum_set f) implies 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 ) )

assume A1: vol A <> 0 ; :: thesis: ( not y in rng (lower_sum_set f) or 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 ) )

assume y in rng (lower_sum_set f) ; :: thesis: 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 )

then consider D3 being Element of divs A such that

A2: D3 in dom (lower_sum_set f) and

A3: y = (lower_sum_set f) . D3 by PARTFUN1:3;

reconsider D3 = D3 as Division of A by INTEGRA1:def 3;

rng D3 <> {} ;

then A4: 1 in dom D3 by FINSEQ_3:32;

A5: len D3 in Seg (len D3) by FINSEQ_1:3;

( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) ; :: thesis: verum

for f being Function of A,REAL st vol A <> 0 & y in rng (lower_sum_set f) holds

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 )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st vol A <> 0 & y in rng (lower_sum_set f) holds

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 )

let f be Function of A,REAL; :: thesis: ( vol A <> 0 & y in rng (lower_sum_set f) implies 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 ) )

assume A1: vol A <> 0 ; :: thesis: ( not y in rng (lower_sum_set f) or 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 ) )

assume y in rng (lower_sum_set f) ; :: thesis: 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 )

then consider D3 being Element of divs A such that

A2: D3 in dom (lower_sum_set f) and

A3: y = (lower_sum_set f) . D3 by PARTFUN1:3;

reconsider D3 = D3 as Division of A by INTEGRA1:def 3;

rng D3 <> {} ;

then A4: 1 in dom D3 by FINSEQ_3:32;

A5: len D3 in Seg (len D3) by FINSEQ_1:3;

now :: thesis: 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 )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 )

per cases
( D3 . 1 <> lower_bound A or D3 . 1 = lower_bound A )
;

end;

suppose A6:
D3 . 1 <> lower_bound A
; :: thesis: 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 )

( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )

D3 . 1 in A
by A4, INTEGRA1:6;

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, A3; :: thesis: verum

end;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, A3; :: thesis: verum

suppose A7:
D3 . 1 = lower_bound A
; :: thesis: 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 )

( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )

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 )

( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) ; :: thesis: verum

end;( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )

proof

hence
ex D being Division of A st
A8:
(lower_volume (f,D3)) . 1 = (lower_bound (rng (f | (divset (D3,1))))) * (vol (divset (D3,1)))
by A4, INTEGRA1:def 7;

vol A >= 0 by INTEGRA1:9;

then A9: (upper_bound A) - (lower_bound A) > 0 by A1, INTEGRA1:def 5;

A10: y = lower_sum (f,D3) by A3, INTEGRA1:def 11

.= Sum (lower_volume (f,D3)) by INTEGRA1:def 9

.= Sum (((lower_volume (f,D3)) | 1) ^ ((lower_volume (f,D3)) /^ 1)) by RFINSEQ:8 ;

A11: D3 . (len D3) = upper_bound A by INTEGRA1:def 2;

len D3 in dom D3 by A5, FINSEQ_1:def 3;

then A12: len D3 > 1 by A4, A7, A11, A9, SEQ_4:137, XREAL_1:47;

then reconsider D = D3 /^ 1 as increasing FinSequence of REAL by INTEGRA1:34;

A13: len D = (len D3) - 1 by A12, RFINSEQ:def 1;

upper_bound A > lower_bound A by A9, XREAL_1:47;

then len D <> 0 by A7, A13, INTEGRA1:def 2;

then reconsider D = D as non empty increasing FinSequence of REAL ;

A14: len D in dom D by FINSEQ_5:6;

(len D) + 1 = len D3 by A13;

then A15: D . (len D) = upper_bound A by A11, A12, A14, RFINSEQ:def 1;

A16: len D3 >= 1 + 1 by A12, NAT_1:13;

then A17: 2 <= len (lower_volume (f,D3)) by INTEGRA1:def 7;

1 + 1 <= len D3 by A12, NAT_1:13;

then 2 in dom D3 by FINSEQ_3:25;

then A18: D3 . 1 < D3 . 2 by A4, SEQM_3:def 1;

A19: rng D3 c= A by INTEGRA1:def 2;

rng D c= rng D3 by FINSEQ_5:33;

then rng D c= A by A19;

then reconsider D = D as Division of A by A15, INTEGRA1:def 2;

A20: 1 in Seg 1 by FINSEQ_1:1;

A21: 1 <= len (lower_volume (f,D3)) by A12, INTEGRA1:def 7;

A22: len ((lower_volume (f,D3)) | 1) = 1 ;

1 <= len (lower_volume (f,D3)) by A12, INTEGRA1:def 7;

then A23: len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) = ((len (lower_volume (f,D3))) -' 2) + 1 by A17, FINSEQ_6:118

.= ((len D3) -' 2) + 1 by INTEGRA1:def 7

.= ((len D3) - 2) + 1 by A16, XREAL_1:233

.= (len D3) - 1 ;

A24: for i being Nat st 1 <= i & i <= len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) holds

(mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) . i = (lower_volume (f,D)) . i

then ((lower_volume (f,D3)) | 1) . 1 = (lower_volume (f,D3)) . 1 by A20, RFINSEQ:6;

then A45: (lower_volume (f,D3)) | 1 = <*((lower_volume (f,D3)) . 1)*> by A22, FINSEQ_1:40;

A46: 2 -' 1 = 2 - 1 by XREAL_1:233

.= 1 ;

rng D <> {} ;

then 1 in dom D by FINSEQ_3:32;

then A47: D . 1 = D3 . (1 + 1) by A12, RFINSEQ:def 1

.= D3 . 2 ;

D in divs A by INTEGRA1:def 3;

then A48: D in dom (lower_sum_set f) by FUNCT_2:def 1;

len (lower_volume (f,D3)) >= 2 by A16, INTEGRA1:def 7;

then A49: mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3)))) = (lower_volume (f,D3)) /^ 1 by A46, FINSEQ_6:117;

len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) = len (lower_volume (f,D)) by A13, A23, INTEGRA1:def 7;

then A50: (lower_volume (f,D3)) /^ 1 = lower_volume (f,D) by A49, A24, FINSEQ_1:14;

vol (divset (D3,1)) = (upper_bound (divset (D3,1))) - (lower_bound (divset (D3,1))) by INTEGRA1:def 5

.= (upper_bound (divset (D3,1))) - (lower_bound A) by A4, INTEGRA1:def 4

.= (D3 . 1) - (lower_bound A) by A4, INTEGRA1:def 4

.= 0 by A7 ;

then y = 0 + (Sum (lower_volume (f,D))) by A10, A45, A8, A50, RVSUM_1:76

.= lower_sum (f,D) by INTEGRA1:def 9 ;

then y = (lower_sum_set f) . D by INTEGRA1:def 11;

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, A48, A47, A18; :: thesis: verum

end;vol A >= 0 by INTEGRA1:9;

then A9: (upper_bound A) - (lower_bound A) > 0 by A1, INTEGRA1:def 5;

A10: y = lower_sum (f,D3) by A3, INTEGRA1:def 11

.= Sum (lower_volume (f,D3)) by INTEGRA1:def 9

.= Sum (((lower_volume (f,D3)) | 1) ^ ((lower_volume (f,D3)) /^ 1)) by RFINSEQ:8 ;

A11: D3 . (len D3) = upper_bound A by INTEGRA1:def 2;

len D3 in dom D3 by A5, FINSEQ_1:def 3;

then A12: len D3 > 1 by A4, A7, A11, A9, SEQ_4:137, XREAL_1:47;

then reconsider D = D3 /^ 1 as increasing FinSequence of REAL by INTEGRA1:34;

A13: len D = (len D3) - 1 by A12, RFINSEQ:def 1;

upper_bound A > lower_bound A by A9, XREAL_1:47;

then len D <> 0 by A7, A13, INTEGRA1:def 2;

then reconsider D = D as non empty increasing FinSequence of REAL ;

A14: len D in dom D by FINSEQ_5:6;

(len D) + 1 = len D3 by A13;

then A15: D . (len D) = upper_bound A by A11, A12, A14, RFINSEQ:def 1;

A16: len D3 >= 1 + 1 by A12, NAT_1:13;

then A17: 2 <= len (lower_volume (f,D3)) by INTEGRA1:def 7;

1 + 1 <= len D3 by A12, NAT_1:13;

then 2 in dom D3 by FINSEQ_3:25;

then A18: D3 . 1 < D3 . 2 by A4, SEQM_3:def 1;

A19: rng D3 c= A by INTEGRA1:def 2;

rng D c= rng D3 by FINSEQ_5:33;

then rng D c= A by A19;

then reconsider D = D as Division of A by A15, INTEGRA1:def 2;

A20: 1 in Seg 1 by FINSEQ_1:1;

A21: 1 <= len (lower_volume (f,D3)) by A12, INTEGRA1:def 7;

A22: len ((lower_volume (f,D3)) | 1) = 1 ;

1 <= len (lower_volume (f,D3)) by A12, INTEGRA1:def 7;

then A23: len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) = ((len (lower_volume (f,D3))) -' 2) + 1 by A17, FINSEQ_6:118

.= ((len D3) -' 2) + 1 by INTEGRA1:def 7

.= ((len D3) - 2) + 1 by A16, XREAL_1:233

.= (len D3) - 1 ;

A24: for i being Nat st 1 <= i & i <= len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) holds

(mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) . i = (lower_volume (f,D)) . i

proof

1 in dom (lower_volume (f,D3))
by A21, FINSEQ_3:25;
let i be Nat; :: thesis: ( 1 <= i & i <= len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) implies (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) . i = (lower_volume (f,D)) . i )

assume that

A25: 1 <= i and

A26: i <= len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) ; :: thesis: (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) . i = (lower_volume (f,D)) . i

A27: 1 <= i + 1 by NAT_1:12;

i + 1 <= len D3 by A23, A26, XREAL_1:19;

then A28: i + 1 in Seg (len D3) by A27, FINSEQ_1:1;

then A29: i + 1 in dom D3 by FINSEQ_1:def 3;

A30: divset (D3,(i + 1)) = divset (D,i)

then A43: i <= ((len (lower_volume (f,D3))) - 2) + 1 ;

(mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) . i = (lower_volume (f,D3)) . ((i + 2) - 1) by A17, A25, A43, FINSEQ_6:122

.= (lower_volume (f,D3)) . (i + 1) ;

then A44: (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 A29, INTEGRA1:def 7;

i in Seg (len D) by A13, A23, A25, A26, FINSEQ_1:1;

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 A44, A30, INTEGRA1:def 7; :: thesis: verum

end;assume that

A25: 1 <= i and

A26: i <= len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) ; :: thesis: (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) . i = (lower_volume (f,D)) . i

A27: 1 <= i + 1 by NAT_1:12;

i + 1 <= len D3 by A23, A26, XREAL_1:19;

then A28: i + 1 in Seg (len D3) by A27, FINSEQ_1:1;

then A29: i + 1 in dom D3 by FINSEQ_1:def 3;

A30: divset (D3,(i + 1)) = divset (D,i)

proof

i <= (len (lower_volume (f,D3))) - 1
by A23, A26, INTEGRA1:def 7;
A31:
i + 1 in dom D3
by A28, FINSEQ_1:def 3;

A32: 1 <> i + 1 by A25, NAT_1:13;

then A33: upper_bound (divset (D3,(i + 1))) = D3 . (i + 1) by A31, INTEGRA1:def 4;

A34: i in dom D by A13, A23, A25, A26, FINSEQ_3:25;

then A35: D . i = D3 . (i + 1) by A12, RFINSEQ:def 1;

A36: lower_bound (divset (D3,(i + 1))) = D3 . ((i + 1) - 1) by A32, A31, INTEGRA1:def 4;

end;A32: 1 <> i + 1 by A25, NAT_1:13;

then A33: upper_bound (divset (D3,(i + 1))) = D3 . (i + 1) by A31, INTEGRA1:def 4;

A34: i in dom D by A13, A23, A25, A26, FINSEQ_3:25;

then A35: D . i = D3 . (i + 1) by A12, RFINSEQ:def 1;

A36: lower_bound (divset (D3,(i + 1))) = D3 . ((i + 1) - 1) by A32, A31, INTEGRA1:def 4;

per cases
( i = 1 or i <> 1 )
;

end;

suppose A37:
i = 1
; :: thesis: divset (D3,(i + 1)) = divset (D,i)

then A38:
upper_bound (divset (D,i)) = D . i
by A34, INTEGRA1:def 4;

A39: lower_bound (divset (D,i)) = lower_bound A by A34, A37, INTEGRA1:def 4;

divset (D3,(i + 1)) = [.(lower_bound A),(D . i).] by A7, A33, A36, A35, A37, INTEGRA1:4;

hence divset (D3,(i + 1)) = divset (D,i) by A39, A38, INTEGRA1:4; :: thesis: verum

end;A39: lower_bound (divset (D,i)) = lower_bound A by A34, A37, INTEGRA1:def 4;

divset (D3,(i + 1)) = [.(lower_bound A),(D . i).] by A7, A33, A36, A35, A37, INTEGRA1:4;

hence divset (D3,(i + 1)) = divset (D,i) by A39, A38, INTEGRA1:4; :: thesis: verum

suppose A40:
i <> 1
; :: thesis: divset (D3,(i + 1)) = divset (D,i)

then
i - 1 in dom D
by A34, INTEGRA1:7;

then A41: D . (i - 1) = D3 . ((i - 1) + 1) by A12, RFINSEQ:def 1

.= D3 . i ;

A42: upper_bound (divset (D,i)) = D . i by A34, A40, INTEGRA1:def 4;

lower_bound (divset (D,i)) = D . (i - 1) by A34, A40, INTEGRA1:def 4;

then divset (D3,(i + 1)) = [.(lower_bound (divset (D,i))),(upper_bound (divset (D,i))).] by A33, A36, A35, A42, A41, INTEGRA1:4;

hence divset (D3,(i + 1)) = divset (D,i) by INTEGRA1:4; :: thesis: verum

end;then A41: D . (i - 1) = D3 . ((i - 1) + 1) by A12, RFINSEQ:def 1

.= D3 . i ;

A42: upper_bound (divset (D,i)) = D . i by A34, A40, INTEGRA1:def 4;

lower_bound (divset (D,i)) = D . (i - 1) by A34, A40, INTEGRA1:def 4;

then divset (D3,(i + 1)) = [.(lower_bound (divset (D,i))),(upper_bound (divset (D,i))).] by A33, A36, A35, A42, A41, INTEGRA1:4;

hence divset (D3,(i + 1)) = divset (D,i) by INTEGRA1:4; :: thesis: verum

then A43: i <= ((len (lower_volume (f,D3))) - 2) + 1 ;

(mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) . i = (lower_volume (f,D3)) . ((i + 2) - 1) by A17, A25, A43, FINSEQ_6:122

.= (lower_volume (f,D3)) . (i + 1) ;

then A44: (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 A29, INTEGRA1:def 7;

i in Seg (len D) by A13, A23, A25, A26, FINSEQ_1:1;

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 A44, A30, INTEGRA1:def 7; :: thesis: verum

then ((lower_volume (f,D3)) | 1) . 1 = (lower_volume (f,D3)) . 1 by A20, RFINSEQ:6;

then A45: (lower_volume (f,D3)) | 1 = <*((lower_volume (f,D3)) . 1)*> by A22, FINSEQ_1:40;

A46: 2 -' 1 = 2 - 1 by XREAL_1:233

.= 1 ;

rng D <> {} ;

then 1 in dom D by FINSEQ_3:32;

then A47: D . 1 = D3 . (1 + 1) by A12, RFINSEQ:def 1

.= D3 . 2 ;

D in divs A by INTEGRA1:def 3;

then A48: D in dom (lower_sum_set f) by FUNCT_2:def 1;

len (lower_volume (f,D3)) >= 2 by A16, INTEGRA1:def 7;

then A49: mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3)))) = (lower_volume (f,D3)) /^ 1 by A46, FINSEQ_6:117;

len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) = len (lower_volume (f,D)) by A13, A23, INTEGRA1:def 7;

then A50: (lower_volume (f,D3)) /^ 1 = lower_volume (f,D) by A49, A24, FINSEQ_1:14;

vol (divset (D3,1)) = (upper_bound (divset (D3,1))) - (lower_bound (divset (D3,1))) by INTEGRA1:def 5

.= (upper_bound (divset (D3,1))) - (lower_bound A) by A4, INTEGRA1:def 4

.= (D3 . 1) - (lower_bound A) by A4, INTEGRA1:def 4

.= 0 by A7 ;

then y = 0 + (Sum (lower_volume (f,D))) by A10, A45, A8, A50, RVSUM_1:76

.= lower_sum (f,D) by INTEGRA1:def 9 ;

then y = (lower_sum_set f) . D by INTEGRA1:def 11;

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, A48, A47, A18; :: thesis: verum

( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) ; :: thesis: verum

( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) ; :: thesis: verum