let A be closed-interval Subset of REAL ; :: thesis: for D1 being Division of A
for f being Function of A,REAL
for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds
( ( for i being Element of NAT st i in Seg (len D1) holds
divset MD1,(i + 1) = divset D1,i ) & upper_volume f,D1 = (upper_volume f,MD1) /^ 1 & lower_volume f,D1 = (lower_volume f,MD1) /^ 1 )
let D1 be Division of A; :: thesis: for f being Function of A,REAL
for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds
( ( for i being Element of NAT st i in Seg (len D1) holds
divset MD1,(i + 1) = divset D1,i ) & upper_volume f,D1 = (upper_volume f,MD1) /^ 1 & lower_volume f,D1 = (lower_volume f,MD1) /^ 1 )
let f be Function of A,REAL ; :: thesis: for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds
( ( for i being Element of NAT st i in Seg (len D1) holds
divset MD1,(i + 1) = divset D1,i ) & upper_volume f,D1 = (upper_volume f,MD1) /^ 1 & lower_volume f,D1 = (lower_volume f,MD1) /^ 1 )
let MD1 be Division of A; :: thesis: ( MD1 = <*(lower_bound A)*> ^ D1 implies ( ( for i being Element of NAT st i in Seg (len D1) holds
divset MD1,(i + 1) = divset D1,i ) & upper_volume f,D1 = (upper_volume f,MD1) /^ 1 & lower_volume f,D1 = (lower_volume f,MD1) /^ 1 ) )
assume A1:
MD1 = <*(lower_bound A)*> ^ D1
; :: thesis: ( ( for i being Element of NAT st i in Seg (len D1) holds
divset MD1,(i + 1) = divset D1,i ) & upper_volume f,D1 = (upper_volume f,MD1) /^ 1 & lower_volume f,D1 = (lower_volume f,MD1) /^ 1 )
then A2: len MD1 =
(len <*(lower_bound A)*>) + (len D1)
by FINSEQ_1:35
.=
1 + (len D1)
by FINSEQ_1:56
;
thus A3:
for i being Element of NAT st i in Seg (len D1) holds
divset MD1,(i + 1) = divset D1,i
:: thesis: ( upper_volume f,D1 = (upper_volume f,MD1) /^ 1 & lower_volume f,D1 = (lower_volume f,MD1) /^ 1 )proof
let i be
Element of
NAT ;
:: thesis: ( i in Seg (len D1) implies divset MD1,(i + 1) = divset D1,i )
assume A4:
i in Seg (len D1)
;
:: thesis: divset MD1,(i + 1) = divset D1,i
then A5:
( 1
<= i &
i <= len D1 )
by FINSEQ_1:3;
A6:
i in dom D1
by A4, FINSEQ_1:def 3;
A7:
1
<= i + 1
by NAT_1:11;
i + 1
<= (len D1) + 1
by A5, XREAL_1:8;
then
i + 1
<= (len D1) + (len <*(lower_bound A)*>)
by FINSEQ_1:56;
then
i + 1
<= len MD1
by A1, FINSEQ_1:35;
then A8:
i + 1
in dom MD1
by A7, FINSEQ_3:27;
A9:
divset D1,
i = [.(lower_bound (divset D1,i)),(upper_bound (divset D1,i)).]
by INTEGRA1:5;
(
lower_bound (divset D1,i) = lower_bound (divset MD1,(i + 1)) &
upper_bound (divset D1,i) = upper_bound (divset MD1,(i + 1)) )
proof
per cases
( i = 1 or i <> 1 )
;
suppose A10:
i = 1
;
:: thesis: ( lower_bound (divset D1,i) = lower_bound (divset MD1,(i + 1)) & upper_bound (divset D1,i) = upper_bound (divset MD1,(i + 1)) )
i + 1
> 1
by A5, NAT_1:13;
then A11:
(
lower_bound (divset MD1,(i + 1)) = MD1 . ((i + 1) - 1) &
upper_bound (divset MD1,(i + 1)) = MD1 . (i + 1) )
by A8, INTEGRA1:def 5;
then A12:
lower_bound (divset MD1,(i + 1)) = lower_bound A
by A1, A10, FINSEQ_1:58;
MD1 . (i + 1) =
MD1 . (i + (len <*(lower_bound A)*>))
by FINSEQ_1:57
.=
D1 . i
by A1, A6, FINSEQ_1:def 7
;
hence
(
lower_bound (divset D1,i) = lower_bound (divset MD1,(i + 1)) &
upper_bound (divset D1,i) = upper_bound (divset MD1,(i + 1)) )
by A6, A10, A11, A12, INTEGRA1:def 5;
:: thesis: verum end; suppose A13:
i <> 1
;
:: thesis: ( lower_bound (divset D1,i) = lower_bound (divset MD1,(i + 1)) & upper_bound (divset D1,i) = upper_bound (divset MD1,(i + 1)) )A14:
i + 1
> 1
by A5, NAT_1:13;
A15:
i - 1
in dom D1
by A6, A13, INTEGRA1:9;
D1 . (i - 1) =
MD1 . ((i - 1) + (len <*(lower_bound A)*>))
by A1, A15, FINSEQ_1:def 7
.=
MD1 . ((i - 1) + 1)
by FINSEQ_1:56
.=
MD1 . ((i + 1) - 1)
;
then A16:
lower_bound (divset D1,i) =
MD1 . ((i + 1) - 1)
by A6, A13, INTEGRA1:def 5
.=
lower_bound (divset MD1,(i + 1))
by A8, A14, INTEGRA1:def 5
;
MD1 . (i + 1) =
MD1 . (i + (len <*(lower_bound A)*>))
by FINSEQ_1:57
.=
D1 . i
by A1, A6, FINSEQ_1:def 7
;
then upper_bound (divset MD1,(i + 1)) =
D1 . i
by A8, A14, INTEGRA1:def 5
.=
upper_bound (divset D1,i)
by A6, A13, INTEGRA1:def 5
;
hence
(
lower_bound (divset D1,i) = lower_bound (divset MD1,(i + 1)) &
upper_bound (divset D1,i) = upper_bound (divset MD1,(i + 1)) )
by A16;
:: thesis: verum end;
end;
hence
divset MD1,
(i + 1) = divset D1,
i
by A9, INTEGRA1:5;
:: thesis: verum
end;
thus
upper_volume f,D1 = (upper_volume f,MD1) /^ 1
:: thesis: lower_volume f,D1 = (lower_volume f,MD1) /^ 1proof
set D2 =
D1;
set MD2 =
MD1;
A17:
len (upper_volume f,D1) = len ((upper_volume f,MD1) /^ 1)
for
k being
Nat st 1
<= k &
k <= len (upper_volume f,D1) holds
(upper_volume f,D1) . k = ((upper_volume f,MD1) /^ 1) . k
proof
let k be
Nat;
:: thesis: ( 1 <= k & k <= len (upper_volume f,D1) implies (upper_volume f,D1) . k = ((upper_volume f,MD1) /^ 1) . k )
assume A18:
( 1
<= k &
k <= len (upper_volume f,D1) )
;
:: thesis: (upper_volume f,D1) . k = ((upper_volume f,MD1) /^ 1) . k
then
k in Seg (len (upper_volume f,D1))
by FINSEQ_1:3;
then A19:
k in Seg (len D1)
by INTEGRA1:def 7;
then
k in dom D1
by FINSEQ_1:def 3;
then A20:
(upper_volume f,D1) . k =
(upper_bound (rng (f | (divset D1,k)))) * (vol (divset D1,k))
by INTEGRA1:def 7
.=
(upper_bound (rng (f | (divset MD1,(k + 1))))) * (vol (divset D1,k))
by A3, A19
.=
(upper_bound (rng (f | (divset MD1,(k + 1))))) * (vol (divset MD1,(k + 1)))
by A3, A19
;
A21:
1
<= k + 1
by NAT_1:11;
k + 1
<= (len (upper_volume f,D1)) + 1
by A18, XREAL_1:8;
then
k + 1
<= (len D1) + 1
by INTEGRA1:def 7;
then A22:
k + 1
in Seg (len MD1)
by A2, A21, FINSEQ_1:3;
B22:
k + 1
in dom MD1
by A22, FINSEQ_1:def 3;
A23:
k in dom ((upper_volume f,MD1) /^ 1)
by A17, A18, FINSEQ_3:27;
A24:
len ((upper_volume f,MD1) /^ 1) <= len (upper_volume f,MD1)
by FINSEQ_5:28;
1
<= len (upper_volume f,D1)
by A18, XXREAL_0:2;
then
1
<= len (upper_volume f,MD1)
by A17, A24, XXREAL_0:2;
then ((upper_volume f,MD1) /^ 1) . k =
(upper_volume f,MD1) . (k + 1)
by A23, RFINSEQ:def 2
.=
(upper_bound (rng (f | (divset MD1,(k + 1))))) * (vol (divset MD1,(k + 1)))
by B22, INTEGRA1:def 7
;
hence
(upper_volume f,D1) . k = ((upper_volume f,MD1) /^ 1) . k
by A20;
:: thesis: verum
end;
hence
upper_volume f,
D1 = (upper_volume f,MD1) /^ 1
by A17, FINSEQ_1:18;
:: thesis: verum
end;
A25:
len (lower_volume f,D1) = len ((lower_volume f,MD1) /^ 1)
for k being Nat st 1 <= k & k <= len (lower_volume f,D1) holds
(lower_volume f,D1) . k = ((lower_volume f,MD1) /^ 1) . k
proof
let k be
Nat;
:: thesis: ( 1 <= k & k <= len (lower_volume f,D1) implies (lower_volume f,D1) . k = ((lower_volume f,MD1) /^ 1) . k )
assume A26:
( 1
<= k &
k <= len (lower_volume f,D1) )
;
:: thesis: (lower_volume f,D1) . k = ((lower_volume f,MD1) /^ 1) . k
then
k in Seg (len (lower_volume f,D1))
by FINSEQ_1:3;
then A27:
k in Seg (len D1)
by INTEGRA1:def 8;
then
k in dom D1
by FINSEQ_1:def 3;
then A28:
(lower_volume f,D1) . k =
(lower_bound (rng (f | (divset D1,k)))) * (vol (divset D1,k))
by INTEGRA1:def 8
.=
(lower_bound (rng (f | (divset MD1,(k + 1))))) * (vol (divset D1,k))
by A3, A27
.=
(lower_bound (rng (f | (divset MD1,(k + 1))))) * (vol (divset MD1,(k + 1)))
by A3, A27
;
A29:
1
<= k + 1
by NAT_1:11;
A30:
len MD1 =
(len <*(lower_bound A)*>) + (len D1)
by A1, FINSEQ_1:35
.=
(len D1) + 1
by FINSEQ_1:56
;
k + 1
<= (len (lower_volume f,D1)) + 1
by A26, XREAL_1:8;
then
k + 1
<= (len D1) + 1
by INTEGRA1:def 8;
then A31:
k + 1
in Seg (len MD1)
by A29, A30, FINSEQ_1:3;
B31:
k + 1
in dom MD1
by A31, FINSEQ_1:def 3;
A32:
k in dom ((lower_volume f,MD1) /^ 1)
by A25, A26, FINSEQ_3:27;
A33:
len ((lower_volume f,MD1) /^ 1) <= len (lower_volume f,MD1)
by FINSEQ_5:28;
1
<= len ((lower_volume f,MD1) /^ 1)
by A25, A26, XXREAL_0:2;
then
1
<= len (lower_volume f,MD1)
by A33, XXREAL_0:2;
then ((lower_volume f,MD1) /^ 1) . k =
(lower_volume f,MD1) . (k + 1)
by A32, RFINSEQ:def 2
.=
(lower_bound (rng (f | (divset MD1,(k + 1))))) * (vol (divset MD1,(k + 1)))
by B31, INTEGRA1:def 8
;
hence
(lower_volume f,D1) . k = ((lower_volume f,MD1) /^ 1) . k
by A28;
:: thesis: verum
end;
hence
lower_volume f,D1 = (lower_volume f,MD1) /^ 1
by A25, FINSEQ_1:18; :: thesis: verum