let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A holds Sum (lower_volume ((chi (A,A)),D)) = vol A
let D be Division of A; :: thesis: Sum (lower_volume ((chi (A,A)),D)) = vol A
deffunc H1( Nat) -> Element of REAL = In ((vol (divset (D,$1))),REAL);
consider p being FinSequence of REAL such that
A1: ( len p = len D & ( for i being Nat st i in dom p holds
p . i = H1(i) ) ) from FINSEQ_2:sch 1();
 A2: dom p = Seg (len D) by A1, FINSEQ_1:def 3;
A3: for i being Element of NAT st i in Seg (len D) holds
p . i = (upper_bound (divset (D,i))) - (lower_bound (divset (D,i)))
proof
let i be Element of NAT ; :: thesis: ( i in Seg (len D) implies p . i = (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) )
A4: In ((vol (divset (D,i))),REAL) = vol (divset (D,i)) ;
assume i in Seg (len D) ; :: thesis: p . i = (upper_bound (divset (D,i))) - (lower_bound (divset (D,i)))
hence p . i = (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by A1, A2, A4; :: thesis: verum
end;
(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 reconsider k = (len D) - 1 as Element of NAT ;
deffunc H2( Nat) -> Element of REAL = In ((lower_bound (divset (D,($1 + 1)))),REAL);
deffunc H3( Nat) -> Element of REAL = In ((upper_bound (divset (D,$1))),REAL);
consider s1 being FinSequence of REAL such that
A5: ( len s1 = k & ( for i being Nat st i in dom s1 holds
s1 . i = H3(i) ) ) from FINSEQ_2:sch 1();
 consider s2 being FinSequence of REAL such that
A6: ( len s2 = k & ( for i being Nat st i in dom s2 holds
s2 . i = H2(i) ) ) from FINSEQ_2:sch 1();
 A7: dom s2 = Seg k by A6, FINSEQ_1:def 3;
reconsider ub = upper_bound A, lb = lower_bound A as Element of REAL by XREAL_0:def 1;
( len (s1 ^ <*(upper_bound A)*>) = len (<*(lower_bound A)*> ^ s2) & len (s1 ^ <*(upper_bound A)*>) = len p & ( for i being Element of NAT st i in dom (s1 ^ <*(upper_bound A)*>) holds
p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i) ) )
proof
dom <*(upper_bound A)*> = Seg 1 by FINSEQ_1:def 8;
then len <*(upper_bound A)*> = 1 by FINSEQ_1:def 3;
then A8: len (s1 ^ <*(upper_bound A)*>) = k + 1 by A5, FINSEQ_1:22;
dom <*(lower_bound A)*> = Seg 1 by FINSEQ_1:def 8;
then len <*(lower_bound A)*> = 1 by FINSEQ_1:def 3;
hence A9: len (s1 ^ <*(upper_bound A)*>) = len (<*(lower_bound A)*> ^ s2) by A6, A8, FINSEQ_1:22; :: thesis: ( len (s1 ^ <*(upper_bound A)*>) = len p & ( for i being Element of NAT st i in dom (s1 ^ <*(upper_bound A)*>) holds
p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i) ) )
thus len (s1 ^ <*(upper_bound A)*>) = len p by A1, A8; :: thesis: for i being Element of NAT st i in dom (s1 ^ <*(upper_bound A)*>) holds
p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i)
let i be Element of NAT ; :: thesis: ( i in dom (s1 ^ <*(upper_bound A)*>) implies p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i) )
A10: In ((upper_bound (divset (D,i))),REAL) = upper_bound (divset (D,i)) ;
A11: In ((lower_bound (divset (D,i))),REAL) = lower_bound (divset (D,i)) ;
assume A12: i in dom (s1 ^ <*(upper_bound A)*>) ; :: thesis: p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i)
then A13: (s1 ^ <*ub*>) /. i = (s1 ^ <*ub*>) . i by PARTFUN1:def 6;
i in Seg (len (s1 ^ <*(upper_bound A)*>)) by A12, FINSEQ_1:def 3;
then i in dom (<*(lower_bound A)*> ^ s2) by A9, FINSEQ_1:def 3;
then A14: (<*lb*> ^ s2) /. i = (<*(lower_bound A)*> ^ s2) . i by PARTFUN1:def 6;
A15: ( len D = 1 or not len D is trivial ) by NAT_2:def 1;
now :: thesis: p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i)
per cases ( len D = 1 or len D >= 2 ) by A15, NAT_2:29;
suppose A16: len D = 1 ; :: thesis: p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i)
then A17: i in Seg 1 by A8, A12, FINSEQ_1:def 3;
then A18: i = 1 by FINSEQ_1:2, TARSKI:def 1;
s1 = {} by A5, A16;
then s1 ^ <*(upper_bound A)*> = <*(upper_bound A)*> by FINSEQ_1:34;
then A19: (s1 ^ <*ub*>) /. i = upper_bound A by A13, A18;
A20: i in dom D by A16, A17, FINSEQ_1:def 3;
s2 = {} by A6, A16;
then <*(lower_bound A)*> ^ s2 = <*(lower_bound A)*> by FINSEQ_1:34;
then A21: (<*lb*> ^ s2) /. i = lower_bound A by A14, A18;
D . i = upper_bound A by A16, A18, Def1;
then A22: upper_bound (divset (D,i)) = upper_bound A by A18, A20, Def3;
p . i = (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by A3, A16, A17;
hence p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i) by A18, A20, A19, A21, A22, Def3; :: thesis: verum
end;
suppose A23: len D >= 2 ; :: thesis: p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i)
1 = 2 - 1 ;
then A24: k >= 1 by A23, XREAL_1:9;
now :: thesis: p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i)
per cases ( i = 1 or i = len D or ( i <> 1 & i <> len D ) ) ;
suppose A25: i = 1 ; :: thesis: p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i)
then A26: i in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
then i in dom <*(lower_bound A)*> by FINSEQ_1:def 8;
then (<*(lower_bound A)*> ^ s2) . i = <*(lower_bound A)*> . i by FINSEQ_1:def 7;
then A27: (<*(lower_bound A)*> ^ s2) . i = lower_bound A by A25;
Seg 1 c= Seg k by A24, FINSEQ_1:5;
then i in Seg k by A26;
then A28: i in dom s1 by A5, FINSEQ_1:def 3;
then (s1 ^ <*(upper_bound A)*>) . i = s1 . i by FINSEQ_1:def 7;
then A29: (s1 ^ <*ub*>) . i = upper_bound (divset (D,i)) by A5, A28, A10;
A30: i in Seg 2 by A25, FINSEQ_1:2, TARSKI:def 2;
A31: Seg 2 c= Seg (len D) by A23, FINSEQ_1:5;
then i in Seg (len D) by A30;
then A32: i in dom D by FINSEQ_1:def 3;
p . i = (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by A3, A31, A30;
hence p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i) by A13, A14, A25, A32, A29, A27, Def3; :: thesis: verum
end;
suppose A33: i = len D ; :: thesis: p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i)
then i - (len s1) in Seg 1 by A5, FINSEQ_1:2, TARSKI:def 1;
then A34: i - (len s1) in dom <*(upper_bound A)*> by FINSEQ_1:def 8;
i = (i - (len s1)) + (len s1) ;
then (s1 ^ <*(upper_bound A)*>) . i = <*(upper_bound A)*> . (i - (len s1)) by A34, FINSEQ_1:def 7;
then A35: (s1 ^ <*ub*>) /. i = upper_bound A by A5, A13, A33;
A36: i <> 1 by A23, A33;
i in Seg (len D) by A33, FINSEQ_1:3;
then A37: i in dom D by FINSEQ_1:def 3;
p . i = (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by A3, A33, FINSEQ_1:3;
then p . i = (upper_bound (divset (D,i))) - (D . (i - 1)) by A37, A36, Def3;
then A38: p . i = (D . i) - (D . (i - 1)) by A37, A36, Def3;
A39: i - (len <*(lower_bound A)*>) = i - 1 by FINSEQ_1:40;
i - 1 <> 0 by A23, A33;
then A40: i - 1 in Seg k by A33, FINSEQ_1:3;
then A41: i - (len <*(lower_bound A)*>) in dom s2 by A6, A39, FINSEQ_1:def 3;
(len <*(lower_bound A)*>) + (i - (len <*(lower_bound A)*>)) = i ;
then A42: (<*lb*> ^ s2) . i = s2 . (i - 1) by A41, A39, FINSEQ_1:def 7;
reconsider i1 = i - 1 as Nat by A40;
(<*lb*> ^ s2) . i = H2(i1) by A6, A39, A41, A42
.= lower_bound (divset (D,i)) ;
then (<*(lower_bound A)*> ^ s2) . i = D . (i - 1) by A37, A36, Def3;
hence p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i) by A14, A33, A35, A38, Def1; :: thesis: verum
end;
suppose A43: ( i <> 1 & i <> len D ) ; :: thesis: p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i)
(len s1) + (len <*(upper_bound A)*>) = k + 1 by A5, FINSEQ_1:39;
then A44: i in Seg (len D) by A12, FINSEQ_1:def 7;
A45: ( i in dom s1 & i in Seg k & i - 1 in Seg k & (i - 1) + 1 = i & i - (len <*(lower_bound A)*>) in dom s2 )
proof
i <> 0 by A44, FINSEQ_1:1;
then not i is trivial by A43, NAT_2:def 1;
then i >= 1 + 1 by NAT_2:29;
then A46: i - 1 >= 1 by XREAL_1:19;
A47: 1 <= i by A44, FINSEQ_1:1;
i <= len D by A44, FINSEQ_1:1;
then A48: i < k + 1 by A43, XXREAL_0:1;
then A49: i <= k by NAT_1:13;
then i in Seg (len s1) by A5, A47, FINSEQ_1:1;
hence i in dom s1 by FINSEQ_1:def 3; :: thesis: ( i in Seg k & i - 1 in Seg k & (i - 1) + 1 = i & i - (len <*(lower_bound A)*>) in dom s2 )
thus i in Seg k by A47, A49, FINSEQ_1:1; :: thesis: ( i - 1 in Seg k & (i - 1) + 1 = i & i - (len <*(lower_bound A)*>) in dom s2 )
i <= k by A48, NAT_1:13;
then i - 1 <= k - 1 by XREAL_1:9;
then A50: (i - 1) + 0 <= (k - 1) + 1 by XREAL_1:7;
ex j being Nat st i = 1 + j by A47, NAT_1:10;
hence i - 1 in Seg k by A46, A50, FINSEQ_1:1; :: thesis: ( (i - 1) + 1 = i & i - (len <*(lower_bound A)*>) in dom s2 )
then A51: i - (len <*(lower_bound A)*>) in Seg (len s2) by A6, FINSEQ_1:39;
thus (i - 1) + 1 = i ; :: thesis: i - (len <*(lower_bound A)*>) in dom s2
thus i - (len <*(lower_bound A)*>) in dom s2 by A51, FINSEQ_1:def 3; :: thesis: verum
end;
then A52: i - (len <*(lower_bound A)*>) in Seg (len s2) by FINSEQ_1:def 3;
then i - (len <*(lower_bound A)*>) <= len s2 by FINSEQ_1:1;
then A53: i <= (len <*(lower_bound A)*>) + (len s2) by XREAL_1:20;
1 <= i - (len <*(lower_bound A)*>) by A52, FINSEQ_1:1;
then (len <*(lower_bound A)*>) + 1 <= i by XREAL_1:19;
then (<*(lower_bound A)*> ^ s2) . i = s2 . (i - (len <*(lower_bound A)*>)) by A53, FINSEQ_1:23;
then (<*(lower_bound A)*> ^ s2) . i = s2 . (i - 1) by FINSEQ_1:39;
then A54: (<*(lower_bound A)*> ^ s2) . i = lower_bound (divset (D,i)) by A6, A7, A45, A11;
(s1 ^ <*(upper_bound A)*>) . i = s1 . i by A45, FINSEQ_1:def 7;
then (s1 ^ <*(upper_bound A)*>) . i = upper_bound (divset (D,i)) by A5, A45, A10;
hence p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i) by A3, A13, A14, A44, A54; :: thesis: verum
end;
end;
end;
hence p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i) ; :: thesis: verum
end;
end;
end;
hence p . i = ((s1 ^ <*ub*>) /. i) - ((<*lb*> ^ s2) /. i) ; :: thesis: verum
end;
then Sum p = (Sum (s1 ^ <*ub*>)) - (Sum (<*lb*> ^ s2)) by Th20;
then Sum p = ((Sum s1) + (upper_bound A)) - (Sum (<*lb*> ^ s2)) by RVSUM_1:74;
then A55: Sum p = ((Sum s1) + (upper_bound A)) - ((lower_bound A) + (Sum s2)) by RVSUM_1:76;
A56: dom s1 = Seg k by A5, FINSEQ_1:def 3;
A57: for i being Element of NAT st i in Seg k holds
upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))
proof
let i be Element of NAT ; :: thesis: ( i in Seg k implies upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) )
A58: 1 + 0 <= i + 1 by XREAL_1:7;
assume A59: i in Seg k ; :: thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))
then i <= k by FINSEQ_1:1;
then i + 1 <= k + 1 by XREAL_1:7;
then i + 1 in Seg (len D) by A58, FINSEQ_1:1;
then A60: i + 1 in dom D by FINSEQ_1:def 3;
k + 1 = len D ;
then k <= len D by NAT_1:11;
then Seg k c= Seg (len D) by FINSEQ_1:5;
then i in Seg (len D) by A59;
then A61: i in dom D by FINSEQ_1:def 3;
A62: (i + 1) - 1 = i ;
now :: thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))
per cases ( i = 1 or i <> 1 ) ;
end;
end;
hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) ; :: thesis: verum
end;
for i being Nat st i in dom s1 holds
s1 . i = s2 . i
proof
let i be Nat; :: thesis: ( i in dom s1 implies s1 . i = s2 . i )
A66: In ((upper_bound (divset (D,i))),REAL) = upper_bound (divset (D,i)) ;
A67: In ((lower_bound (divset (D,(i + 1)))),REAL) = lower_bound (divset (D,(i + 1))) ;
assume A68: i in dom s1 ; :: thesis: s1 . i = s2 . i
then s1 . i = upper_bound (divset (D,i)) by A5, A66;
then s1 . i = lower_bound (divset (D,(i + 1))) by A57, A56, A68;
hence s1 . i = s2 . i by A6, A7, A56, A68, A67; :: thesis: verum
end;
then A69: s1 = s2 by A5, A6, FINSEQ_2:9;
A70: len (lower_volume ((chi (A,A)),D)) = len D by Def6;
then A71: dom (lower_volume ((chi (A,A)),D)) = Seg (len D) by FINSEQ_1:def 3;
for i being Nat st i in dom (lower_volume ((chi (A,A)),D)) holds
(lower_volume ((chi (A,A)),D)) . i = p . i
proof
let i be Nat; :: thesis: ( i in dom (lower_volume ((chi (A,A)),D)) implies (lower_volume ((chi (A,A)),D)) . i = p . i )
A72: In ((vol (divset (D,i))),REAL) = vol (divset (D,i)) ;
assume A73: i in dom (lower_volume ((chi (A,A)),D)) ; :: thesis: (lower_volume ((chi (A,A)),D)) . i = p . i
then i in dom D by A70, FINSEQ_3:29;
then (lower_volume ((chi (A,A)),D)) . i = vol (divset (D,i)) by Th17;
hence (lower_volume ((chi (A,A)),D)) . i = p . i by A1, A2, A71, A73, A72; :: thesis: verum
end;
hence Sum (lower_volume ((chi (A,A)),D)) = vol A by A1, A69, A55, A70, FINSEQ_2:9; :: thesis: verum