let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds
f is_integrable_on A
let f be PartFunc of REAL,REAL; :: thesis: ( f | A is non-decreasing & A c= dom f implies f is_integrable_on A )
assume that
A1: f | A is non-decreasing and
A2: A c= dom f ; :: thesis: f is_integrable_on A
A3: for D being Division of A
for k being Element of NAT st k in dom D holds
( 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) & ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) )
proof
let D be Division of A; :: thesis: for k being Element of NAT st k in dom D holds
( 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) & ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) )
let k be Element of NAT ; :: thesis: ( k in dom D implies ( 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) & ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) ) )
assume A4: k in dom D ; :: thesis: ( 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) & ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) )
then A5: ( (upper_volume ((f || A),D)) . k = (upper_bound (rng ((f || A) | (divset (D,k))))) * (vol (divset (D,k))) & (lower_volume ((f || A),D)) . k = (lower_bound (rng ((f || A) | (divset (D,k))))) * (vol (divset (D,k))) ) by INTEGRA1:def 6, INTEGRA1:def 7;
k in Seg (len D) by A4, FINSEQ_1:def 3;
then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;
then A6: k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;
vol (divset (D,k)) = (upper_volume ((chi (A,A)),D)) . k by A4, INTEGRA1:20;
then vol (divset (D,k)) in rng (upper_volume ((chi (A,A)),D)) by A6, FUNCT_1:def 3;
then vol (divset (D,k)) <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 8;
then A7: vol (divset (D,k)) <= delta D by INTEGRA3:def 1;
A8: divset (D,k) c= A by A4, INTEGRA1:8;
then A9: divset (D,k) c= dom f by A2, XBOOLE_1:1;
f | (divset (D,k)) is non-decreasing by A1, A4, INTEGRA1:8, RFUNCT_2:30;
then A10: ( lower_bound (rng (f | (divset (D,k)))) = f . (lower_bound (divset (D,k))) & upper_bound (rng (f | (divset (D,k)))) = f . (upper_bound (divset (D,k))) ) by A9, Th15;
dom (f | (divset (D,k))) = (dom f) /\ (divset (D,k)) by RELAT_1:61
.= divset (D,k) by A2, A8, XBOOLE_1:1, XBOOLE_1:28 ;
then A11: rng (f | (divset (D,k))) <> {} by RELAT_1:42;
A12: rng (f | (divset (D,k))) = rng ((f || A) | (divset (D,k))) by A8, FUNCT_1:51;
rng (f | A) is real-bounded by A1, A2, Th14;
then rng (f | (divset (D,k))) is real-bounded by A12, RELAT_1:70, XXREAL_2:45;
then A13: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= 0 by A10, A11, SEQ_4:11, XREAL_1:48;
vol (divset (D,k)) >= 0 by INTEGRA1:9;
then 0 * (vol (divset (D,k))) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (vol (divset (D,k))) by A13;
hence 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) by A10, A5, A12; :: thesis: ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D)
((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) = ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (vol (divset (D,k))) by A10, A5, A12;
hence ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) by A13, A7, XREAL_1:64; :: thesis: verum
end;
A14: for D being Division of A holds
( (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) & (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 )
proof
let D be Division of A; :: thesis: ( (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) & (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 )
deffunc H1( Nat) -> Element of REAL = In ((f . (upper_bound (divset (D,$1)))),REAL);
consider F1 being FinSequence of REAL such that
A15: ( len F1 = len D & ( for i being Nat st i in dom F1 holds
F1 . i = H1(i) ) ) from FINSEQ_2:sch 1();
 (len D) - 1 in NAT
proof
ex j being Nat st len D = 1 + j by NAT_1:10, NAT_1:14;
hence (len D) - 1 in NAT by ORDINAL1:def 12; :: thesis: verum
end;
then consider k1 being Element of NAT such that
A16: k1 = (len D) - 1 ;
deffunc H2( Nat) -> Element of REAL = In ((f . (lower_bound (divset (D,$1)))),REAL);
consider F2 being FinSequence of REAL such that
A17: ( len F2 = len D & ( for i being Nat st i in dom F2 holds
F2 . i = H2(i) ) ) from FINSEQ_2:sch 1();
 deffunc H3( Nat) -> Element of REAL = In ((f . (upper_bound (divset (D,$1)))),REAL);
A18: dom F2 = Seg (len D) by A17, FINSEQ_1:def 3;
consider F being FinSequence of REAL such that
A19: ( len F = k1 & ( for i being Nat st i in dom F holds
F . i = H3(i) ) ) from FINSEQ_2:sch 1();
 A20: dom F = Seg k1 by A19, FINSEQ_1:def 3;
A21: for i being Nat st 1 <= i & i <= len F2 holds
F2 . i = (<*(f . (lower_bound A))*> ^ F) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len F2 implies F2 . i = (<*(f . (lower_bound A))*> ^ F) . i )
assume that
A22: 1 <= i and
A23: i <= len F2 ; :: thesis: F2 . i = (<*(f . (lower_bound A))*> ^ F) . i
per cases ( i = 1 or i <> 1 ) ;
suppose A24: i = 1 ; :: thesis: F2 . i = (<*(f . (lower_bound A))*> ^ F) . i
A25: i in Seg (len D) by A17, A22, A23, FINSEQ_1:1;
then A26: i in dom D by FINSEQ_1:def 3;
F2 . i = H2(i) by A17, A18, A25
.= f . (lower_bound (divset (D,i)))
.= f . (lower_bound A) by A24, A26, INTEGRA1:def 4 ;
hence F2 . i = (<*(f . (lower_bound A))*> ^ F) . i by A24, FINSEQ_1:41; :: thesis: verum
end;
suppose A27: i <> 1 ; :: thesis: F2 . i = (<*(f . (lower_bound A))*> ^ F) . i
then A28: i > 1 by A22, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then A29: (len <*(f . (lower_bound A))*>) + 1 <= i by FINSEQ_1:39;
A30: i in Seg (len D) by A17, A22, A23, FINSEQ_1:1;
then A31: i in dom D by FINSEQ_1:def 3;
then reconsider k2 = i - 1 as Element of NAT by A27, INTEGRA1:7;
1 + 1 <= k2 + 1 by A28, NAT_1:13;
then A32: 1 <= k2 by XREAL_1:19;
k2 + 1 <= len F2 by A23;
then A33: k2 <= (len D) - 1 by A17, XREAL_1:19;
then A34: k2 in Seg k1 by A16, A32, FINSEQ_1:1;
A35: upper_bound (divset (D,k2)) = D . (i - 1) len F2 = 1 + ((len D) - 1) by A17
.= (len <*(f . (lower_bound A))*>) + (len F) by A16, A19, FINSEQ_1:39 ;
then A37: (<*(f . (lower_bound A))*> ^ F) . i = F . (i - (len <*(f . (lower_bound A))*>)) by A23, A29, FINSEQ_1:23
.= F . (i - 1) by FINSEQ_1:39 ;
F2 . i = H2(i) by A17, A18, A30
.= f . (lower_bound (divset (D,i)))
.= f . (upper_bound (divset (D,k2))) by A27, A31, INTEGRA1:def 4, A35
.= H3(k2) ;
hence F2 . i = (<*(f . (lower_bound A))*> ^ F) . i by A19, A20, A37, A34; :: thesis: verum
end;
end;
end;
len (<*(f . (lower_bound A))*> ^ F) = (len <*(f . (lower_bound A))*>) + (len F) by FINSEQ_1:22
.= 1 + ((len D) - 1) by A16, A19, FINSEQ_1:39
.= len D ;
then A38: F2 = <*(f . (lower_bound A))*> ^ F by A17, A21, FINSEQ_1:14;
( len (upper_volume ((f || A),D)) = len D & len (lower_volume ((f || A),D)) = len D ) by INTEGRA1:def 6, INTEGRA1:def 7;
then A39: Sum ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) = (Sum (upper_volume ((f || A),D))) - (Sum (lower_volume ((f || A),D))) by Th2
.= (upper_sum ((f || A),D)) - (Sum (lower_volume ((f || A),D))) by INTEGRA1:def 8
.= (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) by INTEGRA1:def 9 ;
A40: dom F1 = Seg (len D) by A15, FINSEQ_1:def 3;
A41: for i being Nat st 1 <= i & i <= len F1 holds
F1 . i = (F ^ <*(f . (upper_bound A))*>) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len F1 implies F1 . i = (F ^ <*(f . (upper_bound A))*>) . i )
assume that
A42: 1 <= i and
A43: i <= len F1 ; :: thesis: F1 . i = (F ^ <*(f . (upper_bound A))*>) . i
now :: thesis: F1 . i = (F ^ <*(f . (upper_bound A))*>) . i
per cases ( i <= len F or i > len F ) ;
suppose i <= len F ; :: thesis: F1 . i = (F ^ <*(f . (upper_bound A))*>) . i
then A44: i in Seg (len F) by A42, FINSEQ_1:1;
then A45: F . i = H3(i) by A19, A20
.= f . (upper_bound (divset (D,i))) ;
A46: i in dom F by A19, A20, A44;
i in Seg (len F1) by A42, A43, FINSEQ_1:1;
then F1 . i = H1(i) by A15, A40
.= f . (upper_bound (divset (D,i))) ;
hence F1 . i = (F ^ <*(f . (upper_bound A))*>) . i by A46, A45, FINSEQ_1:def 7; :: thesis: verum
end;
suppose i > len F ; :: thesis: F1 . i = (F ^ <*(f . (upper_bound A))*>) . i
then A47: i >= (len F) + 1 by NAT_1:13;
then A48: i = (len F) + 1 by A15, A16, A19, A43, XXREAL_0:1;
A49: i in Seg (len F1) by A42, A43, FINSEQ_1:1;
then A50: i in dom D by A15, FINSEQ_1:def 3;
A51: upper_bound (divset (D,i)) = D . i
proof
hence upper_bound (divset (D,i)) = D . i ; :: thesis: verum
end;
F1 . i = H1(i) by A15, A40, A49
.= f . (upper_bound (divset (D,i))) ;
then F1 . i = f . (D . (len D)) by A15, A16, A19, A43, A47, A51, XXREAL_0:1
.= f . (upper_bound A) by INTEGRA1:def 2 ;
hence F1 . i = (F ^ <*(f . (upper_bound A))*>) . i by A48, FINSEQ_1:42; :: thesis: verum
end;
end;
end;
hence F1 . i = (F ^ <*(f . (upper_bound A))*>) . i ; :: thesis: verum
end;
( len (upper_volume ((f || A),D)) = len D & len (lower_volume ((f || A),D)) = len D ) by INTEGRA1:def 6, INTEGRA1:def 7;
then A52: len ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) = len D by Th2;
A53: len (F1 - F2) = len D by A15, A17, Th2;
A54: for k being Element of NAT st k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) holds
((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((delta D) * (F1 - F2)) . k
proof
let k be Element of NAT ; :: thesis: ( k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) implies ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((delta D) * (F1 - F2)) . k )
assume A55: k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) ; :: thesis: ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((delta D) * (F1 - F2)) . k
then k in Seg (len (F1 - F2)) by A52, A53, FINSEQ_1:def 3;
then A56: k in dom (F1 - F2) by FINSEQ_1:def 3;
A57: k in Seg (len D) by A52, A55, FINSEQ_1:def 3;
then k in dom D by FINSEQ_1:def 3;
then ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) by A3;
then A58: ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) by A55, VALUED_1:13;
A59: F1 . k = H1(k) by A15, A40, A57
.= f . (upper_bound (divset (D,k))) ;
F2 . k = H2(k) by A17, A18, A57
.= f . (lower_bound (divset (D,k))) ;
then ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= (delta D) * ((F1 - F2) . k) by A58, A56, VALUED_1:13, A59;
hence ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((delta D) * (F1 - F2)) . k by RVSUM_1:44; :: thesis: verum
end;
(delta D) * (F1 - F2) = ((delta D) multreal) * (F1 - F2) by RVSUM_1:def 7;
then len ((delta D) * (F1 - F2)) = len (F1 - F2) by FINSEQ_2:33;
then len ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) = len ((delta D) * (F1 - F2)) by A15, A17, A52, Th2;
then A60: Sum ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) <= Sum ((delta D) * (F1 - F2)) by A54, Th3;
len (F ^ <*(f . (upper_bound A))*>) = (len F) + (len <*(f . (upper_bound A))*>) by FINSEQ_1:22
.= ((len D) - 1) + 1 by A16, A19, FINSEQ_1:39
.= len D ;
then F1 = F ^ <*(f . (upper_bound A))*> by A15, A41, FINSEQ_1:14;
then Sum (F1 - F2) = (f . (upper_bound A)) - (f . (lower_bound A)) by A38, Th1;
hence (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) by A39, A60, RVSUM_1:87; :: thesis: (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0
for k being Nat st k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) holds
0 <= ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k
proof
let k be Nat; :: thesis: ( k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) implies 0 <= ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k )
set r = ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k;
A61: ( len (upper_volume ((f || A),D)) = len D & len (lower_volume ((f || A),D)) = len D ) by INTEGRA1:def 6, INTEGRA1:def 7;
assume A62: k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) ; :: thesis: 0 <= ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k
then k in Seg (len ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D)))) by FINSEQ_1:def 3;
then k in Seg (len D) by A61, Th2;
then A63: k in dom D by FINSEQ_1:def 3;
((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k = ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) by A62, VALUED_1:13;
hence 0 <= ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k by A3, A63; :: thesis: verum
end;
hence (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 by A39, RVSUM_1:84; :: thesis: verum
end;
A64: ( f || A is total & (f || A) | A is bounded )
proof
consider x being Element of REAL such that
A65: x in A by SUBSET_1:4;
A66: dom (f || A) = (dom f) /\ A by RELAT_1:61
.= A by A2, XBOOLE_1:28 ;
hence f || A is total by PARTFUN1:def 2; :: thesis: (f || A) | A is bounded
( lower_bound A <= x & x <= upper_bound A ) by A65, INTEGRA2:1;
then A67: lower_bound A <= upper_bound A by XXREAL_0:2;
for x being object st x in A /\ (dom (f || A)) holds
(f || A) . x >= (f || A) . (lower_bound A)
proof
lower_bound A in A by A67, INTEGRA2:1;
then A68: ( lower_bound A in A /\ (dom f) & f . (lower_bound A) = (f | A) . (lower_bound A) ) by A2, A66, FUNCT_1:47, XBOOLE_1:28;
let x be object ; :: thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x >= (f || A) . (lower_bound A) )
assume A69: x in A /\ (dom (f || A)) ; :: thesis: (f || A) . x >= (f || A) . (lower_bound A)
then x in A ;
then A70: x in A /\ (dom f) by A2, XBOOLE_1:28;
reconsider x = x as Element of A by A69;
( x >= lower_bound A & f . x = (f | A) . x ) by A66, FUNCT_1:47, INTEGRA2:1;
hence (f || A) . x >= (f || A) . (lower_bound A) by A1, A70, A68, RFUNCT_2:24; :: thesis: verum
end;
then A71: (f || A) | A is bounded_below by RFUNCT_1:71;
for x being object st x in A /\ (dom (f || A)) holds
(f || A) . x <= (f || A) . (upper_bound A)
proof
upper_bound A in A by A67, INTEGRA2:1;
then A72: ( upper_bound A in A /\ (dom f) & f . (upper_bound A) = (f | A) . (upper_bound A) ) by A2, A66, FUNCT_1:47, XBOOLE_1:28;
let x be object ; :: thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x <= (f || A) . (upper_bound A) )
assume A73: x in A /\ (dom (f || A)) ; :: thesis: (f || A) . x <= (f || A) . (upper_bound A)
then x in A ;
then A74: x in A /\ (dom f) by A2, XBOOLE_1:28;
reconsider x = x as Element of A by A73;
( x <= upper_bound A & f . x = (f | A) . x ) by A66, FUNCT_1:47, INTEGRA2:1;
hence (f || A) . x <= (f || A) . (upper_bound A) by A1, A74, A72, RFUNCT_2:24; :: thesis: verum
end;
then (f || A) | A is bounded_above by RFUNCT_1:70;
hence (f || A) | A is bounded by A71; :: thesis: verum
end;
for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0
proof
let T be DivSequence of A; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0 )
assume A75: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: (lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0
A76: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r
proof
consider x being Element of REAL such that
A77: x in A by SUBSET_1:4;
A78: A = A /\ (dom f) by A2, XBOOLE_1:28;
let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
|.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r )
assume A79: 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r
( lower_bound A <= x & x <= upper_bound A ) by A77, INTEGRA2:1;
then A80: lower_bound A <= upper_bound A by XXREAL_0:2;
then ( lower_bound A in A & upper_bound A in A ) by INTEGRA2:1;
then A81: f . (lower_bound A) <= f . (upper_bound A) by A1, A80, A78, RFUNCT_2:24;
per cases ( f . (lower_bound A) = f . (upper_bound A) or f . (lower_bound A) < f . (upper_bound A) ) by A81, XXREAL_0:1;
suppose A82: f . (lower_bound A) = f . (upper_bound A) ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r
reconsider n = 0 as Nat ;
take n ; :: thesis: for m being Nat st n <= m holds
|.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r
let m be Nat; :: thesis: ( n <= m implies |.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r )
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: |.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r
reconsider D1 = T . mm as Division of A ;
A83: ((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m = ((upper_sum ((f || A),T)) . m) + ((- (lower_sum ((f || A),T))) . m) by SEQ_1:7
.= ((upper_sum ((f || A),T)) . m) + (- ((lower_sum ((f || A),T)) . m)) by SEQ_1:10
.= (upper_sum ((f || A),D1)) + (- ((lower_sum ((f || A),T)) . m)) by INTEGRA2:def 2
.= (upper_sum ((f || A),D1)) + (- (lower_sum ((f || A),D1))) by INTEGRA2:def 3 ;
( (upper_sum ((f || A),D1)) - (lower_sum ((f || A),D1)) <= (delta D1) * ((f . (upper_bound A)) - (f . (lower_bound A))) & (upper_sum ((f || A),D1)) - (lower_sum ((f || A),D1)) >= 0 ) by A14;
hence |.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r by A79, A82, A83, ABSVALUE:def 1; :: thesis: verum
end;
suppose f . (lower_bound A) < f . (upper_bound A) ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r
then A84: (f . (upper_bound A)) - (f . (lower_bound A)) > 0 by XREAL_1:50;
then r / ((f . (upper_bound A)) - (f . (lower_bound A))) > 0 by A79, XREAL_1:139;
then consider n being Nat such that
A85: for m being Nat st n <= m holds
|.(((delta T) . m) - 0).| < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A75, SEQ_2:def 7;
A86: for m being Element of NAT st n <= m holds
(delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A)))
proof
let m be Element of NAT ; :: thesis: ( n <= m implies (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A))) )
assume n <= m ; :: thesis: (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A)))
then A87: |.(((delta T) . m) - 0).| < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A85;
(delta T) . m <= |.((delta T) . m).| by ABSVALUE:4;
hence (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A87, XXREAL_0:2; :: thesis: verum
end;
take n ; :: thesis: for m being Nat st n <= m holds
|.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r
let m be Nat; :: thesis: ( n <= m implies |.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r )
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
reconsider D = T . mm as Division of A ;
A88: |.((upper_sum ((f || A),D)) - (lower_sum ((f || A),D))).| = |.((((upper_sum ((f || A),T)) . mm) - (lower_sum ((f || A),D))) - 0).| by INTEGRA2:def 2
.= |.((((upper_sum ((f || A),T)) . mm) - ((lower_sum ((f || A),T)) . m)) - 0).| by INTEGRA2:def 3
.= |.((((upper_sum ((f || A),T)) . m) + (- ((lower_sum ((f || A),T)) . m))) - 0).|
.= |.((((upper_sum ((f || A),T)) . m) + ((- (lower_sum ((f || A),T))) . m)) - 0).| by SEQ_1:10
.= |.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| by SEQ_1:7 ;
assume n <= m ; :: thesis: |.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r
then (delta T) . mm < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A86;
then ((delta T) . m) * ((f . (upper_bound A)) - (f . (lower_bound A))) < r by A84, XREAL_1:79;
then A89: (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) < r by INTEGRA3:def 2;
(upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) by A14;
then A90: (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) < r by A89, XXREAL_0:2;
(upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 by A14;
hence |.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r by A90, A88, ABSVALUE:def 1; :: thesis: verum
end;
end;
end;
A91: ( upper_sum ((f || A),T) is convergent & lower_sum ((f || A),T) is convergent ) by A64, A75, INTEGRA4:8, INTEGRA4:9;
then (upper_sum ((f || A),T)) - (lower_sum ((f || A),T)) is convergent ;
then lim ((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) = 0 by A76, SEQ_2:def 7;
hence (lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0 by A91, SEQ_2:12; :: thesis: verum
end;
then f || A is integrable by A64, INTEGRA4:12;
hence f is_integrable_on A ; :: thesis: verum