let A be 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) -> Real = vol (divset D,$1);
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: vol (divset D,i) = (upper_bound (divset D,i)) - (lower_bound (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 13; :: thesis: verum
end;
then reconsider k = (len D) - 1 as Element of NAT ;
deffunc H2( Nat) -> Element of REAL = lower_bound (divset D,($1 + 1));
deffunc H3( Nat) -> Element of REAL = upper_bound (divset D,$1);
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;
( 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 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ 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:35;
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:35; :: 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 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ 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 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)
let i be Element of NAT ; :: thesis: ( i in dom (s1 ^ <*(upper_bound A)*>) implies p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i) )
assume A10: i in dom (s1 ^ <*(upper_bound A)*>) ; :: thesis: p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)
then A11: (s1 ^ <*(upper_bound A)*>) /. i = (s1 ^ <*(upper_bound A)*>) . i by PARTFUN1:def 8;
i in Seg (len (s1 ^ <*(upper_bound A)*>)) by A10, FINSEQ_1:def 3;
then i in dom (<*(lower_bound A)*> ^ s2) by A9, FINSEQ_1:def 3;
then A12: (<*(lower_bound A)*> ^ s2) /. i = (<*(lower_bound A)*> ^ s2) . i by PARTFUN1:def 8;
A13: ( len D = 1 or not len D is trivial ) by NAT_2:def 1;
now
per cases ( len D = 1 or len D >= 2 ) by A13, NAT_2:31;
suppose A14: len D = 1 ; :: thesis: p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)
then A15: i in Seg 1 by A8, A10, FINSEQ_1:def 3;
then A16: i = 1 by FINSEQ_1:4, TARSKI:def 1;
s1 = {} by A5, A14;
then s1 ^ <*(upper_bound A)*> = <*(upper_bound A)*> by FINSEQ_1:47;
then A17: (s1 ^ <*(upper_bound A)*>) /. i = upper_bound A by A11, A16, FINSEQ_1:def 8;
A18: i in dom D by A14, A15, FINSEQ_1:def 3;
s2 = {} by A6, A14;
then <*(lower_bound A)*> ^ s2 = <*(lower_bound A)*> by FINSEQ_1:47;
then A19: (<*(lower_bound A)*> ^ s2) /. i = lower_bound A by A12, A16, FINSEQ_1:def 8;
D . i = upper_bound A by A14, A16, Def2;
then A20: upper_bound (divset D,i) = upper_bound A by A16, A18, Def5;
p . i = (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by A3, A14, A15;
hence p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i) by A16, A18, A17, A19, A20, Def5; :: thesis: verum
end;
suppose A21: len D >= 2 ; :: thesis: p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)
1 = 2 - 1 ;
then A22: k >= 1 by A21, XREAL_1:11;
now
per cases ( i = 1 or i = len D or ( i <> 1 & i <> len D ) ) ;
suppose A23: i = 1 ; :: thesis: p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)
then A24: i in Seg 1 by FINSEQ_1:4, 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 A25: (<*(lower_bound A)*> ^ s2) . i = lower_bound A by A23, FINSEQ_1:def 8;
Seg 1 c= Seg k by A22, FINSEQ_1:7;
then i in Seg k by A24;
then A26: i in dom s1 by A5, FINSEQ_1:def 3;
then (s1 ^ <*(upper_bound A)*>) . i = s1 . i by FINSEQ_1:def 7;
then A27: (s1 ^ <*(upper_bound A)*>) . i = upper_bound (divset D,i) by A5, A26;
A28: i in Seg 2 by A23, FINSEQ_1:4, TARSKI:def 2;
A29: Seg 2 c= Seg (len D) by A21, FINSEQ_1:7;
then i in Seg (len D) by A28;
then A30: i in dom D by FINSEQ_1:def 3;
p . i = (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by A3, A29, A28;
hence p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i) by A11, A12, A23, A30, A27, A25, Def5; :: thesis: verum
end;
suppose A31: i = len D ; :: thesis: p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)
then i - (len s1) in Seg 1 by A5, FINSEQ_1:4, TARSKI:def 1;
then A32: 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 A32, FINSEQ_1:def 7;
then A33: (s1 ^ <*(upper_bound A)*>) /. i = upper_bound A by A5, A11, A31, FINSEQ_1:def 8;
A34: i <> 1 by A21, A31;
i in Seg (len D) by A31, FINSEQ_1:5;
then A35: i in dom D by FINSEQ_1:def 3;
p . i = (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by A3, A31, FINSEQ_1:5;
then p . i = (upper_bound (divset D,i)) - (D . (i - 1)) by A35, A34, Def5;
then A36: p . i = (D . i) - (D . (i - 1)) by A35, A34, Def5;
A37: i - (len <*(lower_bound A)*>) = i - 1 by FINSEQ_1:57;
i - 1 <> 0 by A21, A31;
then i - 1 in Seg k by A31, FINSEQ_1:5;
then A38: i - (len <*(lower_bound A)*>) in dom s2 by A6, A37, FINSEQ_1:def 3;
A39: (len <*(lower_bound A)*>) + (i - (len <*(lower_bound A)*>)) = i ;
then (<*(lower_bound A)*> ^ s2) . i = s2 . (i - (len <*(lower_bound A)*>)) by A38, FINSEQ_1:def 7;
then (<*(lower_bound A)*> ^ s2) . i = lower_bound (divset D,i) by A6, A37, A39, A38;
then (<*(lower_bound A)*> ^ s2) . i = D . (i - 1) by A35, A34, Def5;
hence p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i) by A12, A31, A33, A36, Def2; :: thesis: verum
end;
suppose A40: ( i <> 1 & i <> len D ) ; :: thesis: p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)
(len s1) + (len <*(upper_bound A)*>) = k + 1 by A5, FINSEQ_1:56;
then A41: i in Seg (len D) by A10, FINSEQ_1:def 7;
A42: ( 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 A41, FINSEQ_1:3;
then not i is trivial by A40, NAT_2:def 1;
then i >= 1 + 1 by NAT_2:31;
then A43: i - 1 >= 1 by XREAL_1:21;
A44: 1 <= i by A41, FINSEQ_1:3;
i <= len D by A41, FINSEQ_1:3;
then A45: i < k + 1 by A40, XXREAL_0:1;
then A46: i <= k by NAT_1:13;
then i in Seg (len s1) by A5, A44, FINSEQ_1:3;
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 A44, A46, FINSEQ_1:3; :: thesis: ( i - 1 in Seg k & (i - 1) + 1 = i & i - (len <*(lower_bound A)*>) in dom s2 )
i <= k by A45, NAT_1:13;
then i - 1 <= k - 1 by XREAL_1:11;
then A47: (i - 1) + 0 <= (k - 1) + 1 by XREAL_1:9;
ex j being Nat st i = 1 + j by A44, NAT_1:10;
hence i - 1 in Seg k by A43, A47, FINSEQ_1:3; :: thesis: ( (i - 1) + 1 = i & i - (len <*(lower_bound A)*>) in dom s2 )
then A48: i - (len <*(lower_bound A)*>) in Seg (len s2) by A6, FINSEQ_1:56;
thus (i - 1) + 1 = i ; :: thesis: i - (len <*(lower_bound A)*>) in dom s2
thus i - (len <*(lower_bound A)*>) in dom s2 by A48, FINSEQ_1:def 3; :: thesis: verum
end;
then A49: 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:3;
then A50: i <= (len <*(lower_bound A)*>) + (len s2) by XREAL_1:22;
1 <= i - (len <*(lower_bound A)*>) by A49, FINSEQ_1:3;
then (len <*(lower_bound A)*>) + 1 <= i by XREAL_1:21;
then (<*(lower_bound A)*> ^ s2) . i = s2 . (i - (len <*(lower_bound A)*>)) by A50, FINSEQ_1:36;
then (<*(lower_bound A)*> ^ s2) . i = s2 . (i - 1) by FINSEQ_1:56;
then A51: (<*(lower_bound A)*> ^ s2) . i = lower_bound (divset D,i) by A6, A7, A42;
(s1 ^ <*(upper_bound A)*>) . i = s1 . i by A42, FINSEQ_1:def 7;
then (s1 ^ <*(upper_bound A)*>) . i = upper_bound (divset D,i) by A5, A42;
hence p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i) by A3, A11, A12, A41, A51; :: thesis: verum
end;
end;
end;
hence p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i) ; :: thesis: verum
end;
end;
end;
hence p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i) ; :: thesis: verum
end;
then Sum p = (Sum (s1 ^ <*(upper_bound A)*>)) - (Sum (<*(lower_bound A)*> ^ s2)) by Th24;
then Sum p = ((Sum s1) + (upper_bound A)) - (Sum (<*(lower_bound A)*> ^ s2)) by RVSUM_1:104;
then A52: Sum p = ((Sum s1) + (upper_bound A)) - ((lower_bound A) + (Sum s2)) by RVSUM_1:106;
A53: dom s1 = Seg k by A5, FINSEQ_1:def 3;
A54: 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)) )
A55: 1 + 0 <= i + 1 by XREAL_1:9;
assume A56: i in Seg k ; :: thesis: upper_bound (divset D,i) = lower_bound (divset D,(i + 1))
then i <= k by FINSEQ_1:3;
then i + 1 <= k + 1 by XREAL_1:9;
then i + 1 in Seg (len D) by A55, FINSEQ_1:3;
then A57: 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:7;
then i in Seg (len D) by A56;
then A58: i in dom D by FINSEQ_1:def 3;
A59: (i + 1) - 1 = i ;
now
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 )
assume A63: i in dom s1 ; :: thesis: s1 . i = s2 . i
then s1 . i = upper_bound (divset D,i) by A5;
then s1 . i = lower_bound (divset D,(i + 1)) by A54, A53, A63;
hence s1 . i = s2 . i by A6, A7, A53, A63; :: thesis: verum
end;
then A64: s1 = s2 by A5, A6, FINSEQ_2:10;
A65: len (lower_volume (chi A,A),D) = len D by Def8;
then A66: 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 )
assume A67: 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 A65, FINSEQ_3:31;
then (lower_volume (chi A,A),D) . i = vol (divset D,i) by Th21;
hence (lower_volume (chi A,A),D) . i = p . i by A1, A2, A66, A67; :: thesis: verum
end;
hence Sum (lower_volume (chi A,A),D) = vol A by A1, A64, A52, A65, FINSEQ_2:10; :: thesis: verum