let A be non empty closed_interval Subset of REAL; :: thesis: for D, E being Division of A
for rho being Function of A,REAL
for K being var_volume of rho,D
for L being var_volume of rho,E st 0 < vol A & D . 1 = lower_bound A & E = D /^ 1 holds
Sum K = Sum L
let D, E be Division of A; :: thesis: for rho being Function of A,REAL
for K being var_volume of rho,D
for L being var_volume of rho,E st 0 < vol A & D . 1 = lower_bound A & E = D /^ 1 holds
Sum K = Sum L
let rho be Function of A,REAL; :: thesis: for K being var_volume of rho,D
for L being var_volume of rho,E st 0 < vol A & D . 1 = lower_bound A & E = D /^ 1 holds
Sum K = Sum L
let K be var_volume of rho,D; :: thesis: for L being var_volume of rho,E st 0 < vol A & D . 1 = lower_bound A & E = D /^ 1 holds
Sum K = Sum L
let L be var_volume of rho,E; :: thesis: ( 0 < vol A & D . 1 = lower_bound A & E = D /^ 1 implies Sum K = Sum L )
assume A1: ( 0 < vol A & D . 1 = lower_bound A & E = D /^ 1 ) ; :: thesis: Sum K = Sum L
0 < len D ;
then A4: 0 + 1 <= len D by NAT_1:13;
A9: len K = ((len D) - 1) + 1 by INTEGR22:def 2
.= (len E) + 1 by A1, A4, RFINSEQ:def 1
.= (len <*0*>) + (len E) by FINSEQ_1:40
.= (len <*0*>) + (len L) by INTEGR22:def 2 ;
A10: dom K = Seg ((len <*0*>) + (len L)) by A9, FINSEQ_1:def 3;
A11: for i being Nat st i in dom <*0*> holds
K . i = <*0*> . i

proof

let i be Nat; :: thesis: ( i in dom <*0*> implies K . i = <*0*> . i )
assume i in dom <*0*> ; :: thesis: K . i = <*0*> . i
then i in Seg (len <*0*>) by FINSEQ_1:def 3;
then i in Seg 1 by FINSEQ_1:40;
then A13: i = 1 by FINSEQ_1:2, TARSKI:def 1;
then A14: i in dom D by FINSEQ_3:25, A4;
A16: vol ((divset (D,i)),rho) = (rho . (upper_bound (divset (D,i)))) - (rho . (lower_bound (divset (D,i)))) by INTEGR22:def 1;
( lower_bound (divset (D,i)) = lower_bound A & upper_bound (divset (D,i)) = lower_bound A ) by A1, A13, A14, INTEGRA1:def 4;
then K . i = |.0.| by A14, INTEGR22:def 2, A16
.= <*0*> . i by A13 ;
hence K . i = <*0*> . i ; :: thesis: verum

end;

for i being Nat st i in dom L holds
K . ((len <*0*>) + i) = L . i

proof

let i be Nat; :: thesis: ( i in dom L implies K . ((len <*0*>) + i) = L . i )
assume a20: i in dom L ; :: thesis: K . ((len <*0*>) + i) = L . i
then i in Seg (len L) by FINSEQ_1:def 3;
then i in Seg (len E) by INTEGR22:def 2;
then A22: i in dom E by FINSEQ_1:def 3;
A26: ( 1 <= i & i <= len L ) by a20, FINSEQ_3:25;
then ( 1 + 0 <= i + 1 & i + 1 <= (len L) + 1 ) by XREAL_1:7;
then ( 1 <= i + 1 & i + 1 <= len K ) by A9, FINSEQ_1:40;
then i + 1 in Seg (len K) ;
then i + 1 in Seg (len D) by INTEGR22:def 2;
then A29: i + 1 in dom D by FINSEQ_1:def 3;
then A30: K . (i + 1) = |.(vol ((divset (D,(i + 1))),rho)).| by INTEGR22:def 2;
A31: vol ((divset (D,(i + 1))),rho) = (rho . (upper_bound (divset (D,(i + 1))))) - (rho . (lower_bound (divset (D,(i + 1))))) by INTEGR22:def 1;
( upper_bound (divset (D,(i + 1))) = upper_bound (divset (E,i)) & lower_bound (divset (D,(i + 1))) = lower_bound (divset (E,i)) )

proof

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

suppose A33: i = 1 ; :: thesis: ( upper_bound (divset (D,(i + 1))) = upper_bound (divset (E,i)) & lower_bound (divset (D,(i + 1))) = lower_bound (divset (E,i)) )

then B35: ( lower_bound (divset (E,i)) = lower_bound A & upper_bound (divset (E,i)) = E . i ) by A22, INTEGRA1:def 4;
( lower_bound (divset (D,(i + 1))) = D . ((i + 1) - 1) & upper_bound (divset (D,(i + 1))) = D . (i + 1) ) by A29, INTEGRA1:def 4, A33;
hence ( upper_bound (divset (D,(i + 1))) = upper_bound (divset (E,i)) & lower_bound (divset (D,(i + 1))) = lower_bound (divset (E,i)) ) by A33, B35, A1, A4, A22, RFINSEQ:def 1; :: thesis: verum

end;

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

then A37: ( lower_bound (divset (E,i)) = E . (i - 1) & upper_bound (divset (E,i)) = E . i ) by A22, INTEGRA1:def 4;
1 < i by A26, A36, XXREAL_0:1;
then ( 1 + 1 <= i & i <= len E ) by INTEGR22:def 2, A26, NAT_1:13;
then A39: ( (1 + 1) - 1 <= i - 1 & i - 1 <= (len E) - 0 ) by XREAL_1:13;
i - 1 is Nat by A26, INT_1:5, ORDINAL1:def 12;
then i - 1 in dom E by FINSEQ_3:25, A39;
then A42: ( lower_bound (divset (E,i)) = D . ((i - 1) + 1) & upper_bound (divset (E,i)) = D . (i + 1) ) by A1, A4, A22, A37, RFINSEQ:def 1;
1 + 0 < i + 1 by A26, XREAL_1:8;
then ( lower_bound (divset (D,(i + 1))) = D . ((i + 1) - 1) & upper_bound (divset (D,(i + 1))) = D . (i + 1) ) by A29, INTEGRA1:def 4;
hence ( upper_bound (divset (D,(i + 1))) = upper_bound (divset (E,i)) & lower_bound (divset (D,(i + 1))) = lower_bound (divset (E,i)) ) by A42; :: thesis: verum

end;

end;

end;

then vol ((divset (D,(i + 1))),rho) = vol ((divset (E,i)),rho) by INTEGR22:def 1, A31;
then K . (i + 1) = L . i by A22, INTEGR22:def 2, A30;
hence K . ((len <*0*>) + i) = L . i by FINSEQ_1:40; :: thesis: verum

end;

then K = <*0*> ^ L by A10, A11, FINSEQ_1:def 7;
hence Sum K = 0 + (Sum L) by RVSUM_1:76
.= Sum L ;
:: thesis: verum