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 H₁( 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 = H₁(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)) )
assume A4: i in Seg (len D) ; :: thesis: p . i = (upper_bound (divset D,i)) - (lower_bound (divset D,i))
vol (divset D,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, A4, A2; :: thesis: verum

end;

(len D) - 1 in NAT

proof

len D >= 1 by NAT_1:14;
then consider j being Nat such that
A5: len D = 1 + j by NAT_1:10;
thus (len D) - 1 in NAT by A5, ORDINAL1:def 13; :: thesis: verum

end;

then reconsider k = (len D) - 1 as Element of NAT ;
deffunc H₂( Nat) -> Element of REAL = upper_bound (divset D,$1);
consider s1 being FinSequence of REAL such that
A6: ( len s1 = k & ( for i being Nat st i in dom s1 holds
s1 . i = H₂(i) ) ) from FINSEQ_2:sch 1();
deffunc H₃( Nat) -> Element of REAL = lower_bound (divset D,($1 + 1));
consider s2 being FinSequence of REAL such that
A8: ( len s2 = k & ( for i being Nat st i in dom s2 holds
s2 . i = H₃(i) ) ) from FINSEQ_2:sch 1();
A9: dom s2 = Seg k by A8, FINSEQ_1:def 3;
A10: 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)) )
assume A11: i in Seg k ; :: thesis: upper_bound (divset D,i) = lower_bound (divset D,(i + 1))
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 A11;
then A12: i in dom D by FINSEQ_1:def 3;
A13: i + 1 in dom D

proof

( 1 <= i & i <= k ) by A11, FINSEQ_1:3;
then ( 1 + 0 <= i + 1 & i + 1 <= k + 1 ) by XREAL_1:9;
then i + 1 in Seg (len D) by FINSEQ_1:3;
hence i + 1 in dom D by FINSEQ_1:def 3; :: thesis: verum

end;

A14: (i + 1) - 1 = i ;

now

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

suppose A15: i = 1 ; :: thesis: upper_bound (divset D,i) = lower_bound (divset D,(i + 1))

then upper_bound (divset D,i) = D . i by A12, Def5;
hence upper_bound (divset D,i) = lower_bound (divset D,(i + 1)) by A13, A14, A15, Def5; :: thesis: verum

end;

suppose A16: i <> 1 ; :: thesis: upper_bound (divset D,i) = lower_bound (divset D,(i + 1))

i >= 1 by A11, FINSEQ_1:3;
then i + 1 >= 1 + 1 by XREAL_1:8;
then A17: i + 1 <> 1 ;
upper_bound (divset D,i) = D . i by A12, A16, Def5;
hence upper_bound (divset D,i) = lower_bound (divset D,(i + 1)) by A13, A14, A17, Def5; :: thesis: verum

end;

end;

end;

hence upper_bound (divset D,i) = lower_bound (divset D,(i + 1)) ; :: thesis: verum

end;

A18: s1 = s2

proof

X: dom s1 = Seg k by A6, FINSEQ_1:def 3;
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 A19: i in dom s1 ; :: thesis: s1 . i = s2 . i
then s1 . i = upper_bound (divset D,i) by A6;
then s1 . i = lower_bound (divset D,(i + 1)) by A10, A19, X;
hence s1 . i = s2 . i by A8, A19, A9, X; :: thesis: verum

end;

hence s1 = s2 by A6, A8, FINSEQ_2:10; :: thesis: verum

end;

A20: ( 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 A21: len <*(upper_bound A)*> = 1 by FINSEQ_1:def 3;
dom <*(lower_bound A)*> = Seg 1 by FINSEQ_1:def 8;
then A22: len <*(lower_bound A)*> = 1 by FINSEQ_1:def 3;
A23: len (s1 ^ <*(upper_bound A)*>) = k + 1 by A6, A21, FINSEQ_1:35;
hence A24: len (s1 ^ <*(upper_bound A)*>) = len (<*(lower_bound A)*> ^ s2) by A8, A22, 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, A23; :: 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 A25: i in dom (s1 ^ <*(upper_bound A)*>) ; :: thesis: p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)
A26: i in dom (<*(lower_bound A)*> ^ s2)

proof

i in Seg (len (s1 ^ <*(upper_bound A)*>)) by A25, FINSEQ_1:def 3;
hence i in dom (<*(lower_bound A)*> ^ s2) by A24, FINSEQ_1:def 3; :: thesis: verum

end;

A27: ( len D = 1 or len D >= 2 )

proof

( len D = 1 or not len D is trivial ) by NAT_2:def 1;
hence ( len D = 1 or len D >= 2 ) by NAT_2:31; :: thesis: verum

end;

A28: (s1 ^ <*(upper_bound A)*>) /. i = (s1 ^ <*(upper_bound A)*>) . i by A25, PARTFUN1:def 8;
A29: (<*(lower_bound A)*> ^ s2) /. i = (<*(lower_bound A)*> ^ s2) . i by A26, PARTFUN1:def 8;

now

per cases ( len D = 1 or len D >= 2 ) by A27;

suppose A30: len D = 1 ; :: thesis: p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)

then A31: i in Seg 1 by A23, A25, FINSEQ_1:def 3;
then A32: i = 1 by FINSEQ_1:4, TARSKI:def 1;
A33: ( i in Seg (len D) & i in dom D ) by A30, A31, FINSEQ_1:def 3;
s1 = {} by A6, A30;
then s1 ^ <*(upper_bound A)*> = <*(upper_bound A)*> by FINSEQ_1:47;
then A34: (s1 ^ <*(upper_bound A)*>) /. i = upper_bound A by A28, A32, FINSEQ_1:def 8;
s2 = {} by A8, A30;
then <*(lower_bound A)*> ^ s2 = <*(lower_bound A)*> by FINSEQ_1:47;
then A35: (<*(lower_bound A)*> ^ s2) /. i = lower_bound A by A29, A32, FINSEQ_1:def 8;
D . i = upper_bound A by A30, A32, Def2;
then A36: upper_bound (divset D,i) = upper_bound A by A32, A33, Def5;
p . i = (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by A3, A30, A31;
hence p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i) by A32, A33, A34, A35, A36, Def5; :: thesis: verum

end;

suppose A37: len D >= 2 ; :: thesis: p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)

A38: k >= 1

proof

1 = 2 - 1 ;
hence k >= 1 by A37, XREAL_1:11; :: thesis: verum

end;

now

per cases ( i = 1 or i = len D or ( i <> 1 & i <> len D ) ) ;

suppose A39: i = 1 ; :: thesis: p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)

A40: ( i in Seg (len D) & i in dom D )

proof

A41: Seg 2 c= Seg (len D) by A37, FINSEQ_1:7;
i in Seg 2 by A39, FINSEQ_1:4, TARSKI:def 2;
hence i in Seg (len D) by A41; :: thesis: i in dom D
hence i in dom D by FINSEQ_1:def 3; :: thesis: verum

end;

A42: ( i in Seg 1 & i in Seg k & i in dom s1 )

proof

A43: Seg 1 c= Seg k by A38, FINSEQ_1:7;
thus i in Seg 1 by A39, FINSEQ_1:4, TARSKI:def 1; :: thesis: ( i in Seg k & i in dom s1 )
hence i in Seg k by A43; :: thesis: i in dom s1
hence i in dom s1 by A6, FINSEQ_1:def 3; :: thesis: verum

end;

then (s1 ^ <*(upper_bound A)*>) . i = s1 . i by FINSEQ_1:def 7;
then A44: (s1 ^ <*(upper_bound A)*>) . i = upper_bound (divset D,i) by A6, A42;
A45: (<*(lower_bound A)*> ^ s2) . i = lower_bound A

proof

i in dom <*(lower_bound A)*> by A42, FINSEQ_1:def 8;
then (<*(lower_bound A)*> ^ s2) . i = <*(lower_bound A)*> . i by FINSEQ_1:def 7;
hence (<*(lower_bound A)*> ^ s2) . i = lower_bound A by A39, FINSEQ_1:def 8; :: thesis: verum

end;

p . i = (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by A3, A40;
hence p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i) by A28, A29, A39, A40, A44, A45, Def5; :: thesis: verum

end;

suppose A46: i = len D ; :: thesis: p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)

A47: ( i in Seg (len D) & i in dom D )

proof

thus i in Seg (len D) by A46, FINSEQ_1:5; :: thesis: i in dom D
hence i in dom D by FINSEQ_1:def 3; :: thesis: verum

end;

A48: ( i - (len s1) = 1 & i - (len s1) in dom <*(upper_bound A)*> & i = (i - (len s1)) + (len s1) & i <> 1 )

proof

thus i - (len s1) = 1 by A6, A46; :: thesis: ( i - (len s1) in dom <*(upper_bound A)*> & i = (i - (len s1)) + (len s1) & i <> 1 )
i - (len s1) in Seg 1 by A6, A46, FINSEQ_1:4, TARSKI:def 1;
hence i - (len s1) in dom <*(upper_bound A)*> by FINSEQ_1:def 8; :: thesis: ( i = (i - (len s1)) + (len s1) & i <> 1 )
thus i = (i - (len s1)) + (len s1) ; :: thesis: i <> 1
thus i <> 1 by A37, A46; :: thesis: verum

end;

then (s1 ^ <*(upper_bound A)*>) . i = <*(upper_bound A)*> . (i - (len s1)) by FINSEQ_1:def 7;
then A49: (s1 ^ <*(upper_bound A)*>) /. i = upper_bound A by A28, A48, FINSEQ_1:def 8;
A50: ( i - (len <*(lower_bound A)*>) = i - 1 & (len <*(lower_bound A)*>) + (i - (len <*(lower_bound A)*>)) = i & i - 1 in Seg k & i - (len <*(lower_bound A)*>) in dom s2 & (i - 1) + 1 = i )

proof

thus A51: i - (len <*(lower_bound A)*>) = i - 1 by FINSEQ_1:57; :: thesis: ( (len <*(lower_bound A)*>) + (i - (len <*(lower_bound A)*>)) = i & i - 1 in Seg k & i - (len <*(lower_bound A)*>) in dom s2 & (i - 1) + 1 = i )
thus (len <*(lower_bound A)*>) + (i - (len <*(lower_bound A)*>)) = i ; :: thesis: ( i - 1 in Seg k & i - (len <*(lower_bound A)*>) in dom s2 & (i - 1) + 1 = i )
( i - 1 <> 0 & i - 1 = k ) by A37, A46;
hence i - 1 in Seg k by FINSEQ_1:5; :: thesis: ( i - (len <*(lower_bound A)*>) in dom s2 & (i - 1) + 1 = i )
hence i - (len <*(lower_bound A)*>) in dom s2 by A8, A51, FINSEQ_1:def 3; :: thesis: (i - 1) + 1 = i
thus (i - 1) + 1 = i ; :: thesis: verum

end;

A52: (<*(lower_bound A)*> ^ s2) . i = D . (i - 1)

proof

(<*(lower_bound A)*> ^ s2) . i = s2 . (i - (len <*(lower_bound A)*>)) by A50, FINSEQ_1:def 7;
then (<*(lower_bound A)*> ^ s2) . i = lower_bound (divset D,i) by A8, A50;
hence (<*(lower_bound A)*> ^ s2) . i = D . (i - 1) by A47, A48, Def5; :: thesis: verum

end;

p . i = (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by A3, A47;
then p . i = (upper_bound (divset D,i)) - (D . (i - 1)) by A47, A48, Def5;
then p . i = (D . i) - (D . (i - 1)) by A47, A48, Def5;
hence p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i) by A29, A46, A49, A52, Def2; :: thesis: verum

end;

suppose A54: ( i <> 1 & i <> len D ) ; :: thesis: p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i)

A55: ( i in Seg (len D) & i in dom D )

proof

A56: (len s1) + (len <*(upper_bound A)*>) = k + 1 by A6, FINSEQ_1:56;
hence i in Seg (len D) by A25, FINSEQ_1:def 7; :: thesis: i in dom D
dom (s1 ^ <*(upper_bound A)*>) = Seg (len D) by A56, FINSEQ_1:def 7;
hence i in dom D by A25, FINSEQ_1:def 3; :: thesis: verum

end;

A57: ( 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

A58: ( 1 <= i & i <= len D ) by A55, FINSEQ_1:3;
then A59: ( 1 <= i & i < k + 1 ) by A54, XXREAL_0:1;
then A60: ( 1 <= i & i <= k ) by NAT_1:13;
then i in Seg (len s1) by A6, 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 A60, FINSEQ_1:3; :: thesis: ( i - 1 in Seg k & (i - 1) + 1 = i & i - (len <*(lower_bound A)*>) in dom s2 )
consider j being Nat such that
A61: i = 1 + j by A58, NAT_1:10;
( i <> 0 & i <> 1 ) by A54, A55, FINSEQ_1:3;
then not i is trivial by NAT_2:def 1;
then ( i >= 2 & i <= k ) by A59, NAT_1:13, NAT_2:31;
then ( i >= 1 + 1 & i - 1 <= k - 1 ) by XREAL_1:11;
then ( i - 1 >= 1 & (i - 1) + 0 <= (k - 1) + 1 ) by XREAL_1:9, XREAL_1:21;
hence i - 1 in Seg k by A61, FINSEQ_1:3; :: thesis: ( (i - 1) + 1 = i & i - (len <*(lower_bound A)*>) in dom s2 )
then A62: i - (len <*(lower_bound A)*>) in Seg (len s2) by A8, 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 A62, FINSEQ_1:def 3; :: thesis: verum

end;

A63: (s1 ^ <*(upper_bound A)*>) . i = D . i

proof

(s1 ^ <*(upper_bound A)*>) . i = s1 . i by A57, FINSEQ_1:def 7;
then (s1 ^ <*(upper_bound A)*>) . i = upper_bound (divset D,i) by A6, A57;
hence (s1 ^ <*(upper_bound A)*>) . i = D . i by A54, A55, Def5; :: thesis: verum

end;

A64: (<*(lower_bound A)*> ^ s2) . i = D . (i - 1)

proof

A65: i - (len <*(lower_bound A)*>) in Seg (len s2) by A57, FINSEQ_1:def 3;
( 1 <= i - (len <*(lower_bound A)*>) & i - (len <*(lower_bound A)*>) <= len s2 ) by A65, FINSEQ_1:3;
then ( (len <*(lower_bound A)*>) + 1 <= i & i <= (len <*(lower_bound A)*>) + (len s2) ) by XREAL_1:21, XREAL_1:22;
then (<*(lower_bound A)*> ^ s2) . i = s2 . (i - (len <*(lower_bound A)*>)) by FINSEQ_1:36;
then (<*(lower_bound A)*> ^ s2) . i = s2 . (i - 1) by FINSEQ_1:56;
then (<*(lower_bound A)*> ^ s2) . i = lower_bound (divset D,i) by A8, A57, A9;
hence (<*(lower_bound A)*> ^ s2) . i = D . (i - 1) by A54, A55, Def5; :: thesis: verum

end;

p . i = (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by A3, A55;
then p . i = (upper_bound (divset D,i)) - (D . (i - 1)) by A54, A55, Def5;
hence p . i = ((s1 ^ <*(upper_bound A)*>) /. i) - ((<*(lower_bound A)*> ^ s2) /. i) by A28, A29, A54, A55, A63, A64, Def5; :: 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;

A67: Sum p = (((Sum s1) + (upper_bound A)) - (lower_bound A)) - (Sum s2)

proof

Sum p = (Sum (s1 ^ <*(upper_bound A)*>)) - (Sum (<*(lower_bound A)*> ^ s2)) by A20, Th24;
then Sum p = ((Sum s1) + (upper_bound A)) - (Sum (<*(lower_bound A)*> ^ s2)) by RVSUM_1:104;
then Sum p = ((Sum s1) + (upper_bound A)) - ((lower_bound A) + (Sum s2)) by RVSUM_1:106;
hence Sum p = (((Sum s1) + (upper_bound A)) - (lower_bound A)) - (Sum s2) ; :: thesis: verum

end;

Sum (lower_volume (chi A,A),D) = Sum p

proof

lower_volume (chi A,A),D = p

proof

A68: ( len (lower_volume (chi A,A),D) = len D & len p = len D ) by A1, Def8;
then X: 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 A69: 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 A68, 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, A69, A2, X; :: thesis: verum

end;

hence lower_volume (chi A,A),D = p by A68, FINSEQ_2:10; :: thesis: verum

end;

hence Sum (lower_volume (chi A,A),D) = Sum p ; :: thesis: verum

end;

hence Sum (lower_volume (chi A,A),D) = vol A by A18, A67; :: thesis: verum