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 () holds
ex D being Division of A st
( D in dom () & y = () . 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 () holds
ex D being Division of A st
( D in dom () & y = () . D & D . 1 > lower_bound A )

let f be Function of A,REAL; :: thesis: ( vol A <> 0 & y in rng () implies ex D being Division of A st
( D in dom () & y = () . D & D . 1 > lower_bound A ) )

assume A1: vol A <> 0 ; :: thesis: ( not y in rng () or ex D being Division of A st
( D in dom () & y = () . D & D . 1 > lower_bound A ) )

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

then consider D3 being Element of divs A such that
A2: D3 in dom () and
A3: y = () . 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 () & y = () . D & D . 1 > lower_bound A )
per cases ( D3 . 1 <> lower_bound A or D3 . 1 = lower_bound A ) ;
suppose A6: D3 . 1 <> lower_bound A ; :: thesis: ex D being Division of A st
( D in dom () & y = () . D & D . 1 > lower_bound A )

D3 . 1 in A by ;
then lower_bound A <= D3 . 1 by INTEGRA2:1;
then D3 . 1 > lower_bound A by ;
hence ex D being Division of A st
( D in dom () & y = () . D & D . 1 > lower_bound A ) by A2, A3; :: thesis: verum
end;
suppose A7: D3 . 1 = lower_bound A ; :: thesis: ex D being Division of A st
( D in dom () & y = () . D & D . 1 > lower_bound A )

ex D being Division of A st
( D in dom () & y = () . D & D . 1 > lower_bound A )
proof
A8: (lower_volume (f,D3)) . 1 = (lower_bound (rng (f | (divset (D3,1))))) * (vol (divset (D3,1))) by ;
vol A >= 0 by INTEGRA1:9;
then A9: (upper_bound A) - () > 0 by ;
A10: y = lower_sum (f,D3) by
.= 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 ;
then A12: len D3 > 1 by ;
then reconsider D = D3 /^ 1 as increasing FinSequence of REAL by INTEGRA1:34;
A13: len D = (len D3) - 1 by ;
upper_bound A > lower_bound A by ;
then len D <> 0 by ;
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 ;
A16: len D3 >= 1 + 1 by ;
then A17: 2 <= len (lower_volume (f,D3)) by INTEGRA1:def 7;
1 + 1 <= len D3 by ;
then 2 in dom D3 by FINSEQ_3:25;
then A18: D3 . 1 < D3 . 2 by ;
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 ;
A20: 1 in Seg 1 by FINSEQ_1:1;
A21: 1 <= len (lower_volume (f,D3)) by ;
A22: len ((lower_volume (f,D3)) | 1) = 1 ;
1 <= len (lower_volume (f,D3)) by ;
then A23: len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) = ((len (lower_volume (f,D3))) -' 2) + 1 by
.= ((len D3) -' 2) + 1 by INTEGRA1:def 7
.= ((len D3) - 2) + 1 by
.= (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
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 ;
then A28: i + 1 in Seg (len D3) by ;
then A29: i + 1 in dom D3 by FINSEQ_1:def 3;
A30: divset (D3,(i + 1)) = divset (D,i)
proof
A31: i + 1 in dom D3 by ;
A32: 1 <> i + 1 by ;
then A33: upper_bound (divset (D3,(i + 1))) = D3 . (i + 1) by ;
A34: i in dom D by ;
then A35: D . i = D3 . (i + 1) by ;
A36: lower_bound (divset (D3,(i + 1))) = D3 . ((i + 1) - 1) by ;
per cases ( i = 1 or i <> 1 ) ;
suppose A37: i = 1 ; :: thesis: divset (D3,(i + 1)) = divset (D,i)
then A38: upper_bound (divset (D,i)) = D . i by ;
A39: lower_bound (divset (D,i)) = lower_bound A by ;
divset (D3,(i + 1)) = [.(),(D . i).] by ;
hence divset (D3,(i + 1)) = divset (D,i) by ; :: thesis: verum
end;
suppose A40: i <> 1 ; :: thesis: divset (D3,(i + 1)) = divset (D,i)
then i - 1 in dom D by ;
then A41: D . (i - 1) = D3 . ((i - 1) + 1) by
.= D3 . i ;
A42: upper_bound (divset (D,i)) = D . i by ;
lower_bound (divset (D,i)) = D . (i - 1) by ;
then divset (D3,(i + 1)) = [.(lower_bound (divset (D,i))),(upper_bound (divset (D,i))).] by ;
hence divset (D3,(i + 1)) = divset (D,i) by INTEGRA1:4; :: thesis: verum
end;
end;
end;
i <= (len (lower_volume (f,D3))) - 1 by ;
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
.= (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 ;
i in Seg (len D) by ;
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 ; :: thesis: verum
end;
1 in dom (lower_volume (f,D3)) by ;
then ((lower_volume (f,D3)) | 1) . 1 = (lower_volume (f,D3)) . 1 by ;
then A45: (lower_volume (f,D3)) | 1 = <*((lower_volume (f,D3)) . 1)*> by ;
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
.= D3 . 2 ;
D in divs A by INTEGRA1:def 3;
then A48: D in dom () by FUNCT_2:def 1;
len (lower_volume (f,D3)) >= 2 by ;
then A49: mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3)))) = (lower_volume (f,D3)) /^ 1 by ;
len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) = len (lower_volume (f,D)) by ;
then A50: (lower_volume (f,D3)) /^ 1 = lower_volume (f,D) by ;
vol (divset (D3,1)) = (upper_bound (divset (D3,1))) - (lower_bound (divset (D3,1))) by INTEGRA1:def 5
.= (upper_bound (divset (D3,1))) - () by
.= (D3 . 1) - () by
.= 0 by A7 ;
then y = 0 + (Sum (lower_volume (f,D))) by
.= lower_sum (f,D) by INTEGRA1:def 9 ;
then y = () . D by INTEGRA1:def 11;
hence ex D being Division of A st
( D in dom () & y = () . D & D . 1 > lower_bound A ) by A7, A48, A47, A18; :: thesis: verum
end;
hence ex D being Division of A st
( D in dom () & y = () . D & D . 1 > lower_bound A ) ; :: thesis: verum
end;
end;
end;
hence ex D being Division of A st
( D in dom () & y = () . D & D . 1 > lower_bound A ) ; :: thesis: verum