let A be non empty closed_interval Subset of REAL; 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; 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; 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; ( 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
; ( ( 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 )
thus A2:
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 )proof
let i be
Element of
NAT ;
( i in Seg (len D1) implies divset (MD1,(i + 1)) = divset (D1,i) )
assume A3:
i in Seg (len D1)
;
divset (MD1,(i + 1)) = divset (D1,i)
then A4:
i in dom D1
by FINSEQ_1:def 3;
i <= len D1
by A3, FINSEQ_1:1;
then
i + 1
<= (len D1) + 1
by XREAL_1:6;
then
i + 1
<= (len D1) + (len <*(lower_bound A)*>)
by FINSEQ_1:39;
then A5:
i + 1
<= len MD1
by A1, FINSEQ_1:22;
1
<= i + 1
by NAT_1:11;
then A6:
i + 1
in dom MD1
by A5, FINSEQ_3:25;
A7:
1
<= i
by A3, FINSEQ_1:1;
A8:
(
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 A9:
i = 1
;
( lower_bound (divset (D1,i)) = lower_bound (divset (MD1,(i + 1))) & upper_bound (divset (D1,i)) = upper_bound (divset (MD1,(i + 1))) )A10:
i + 1
> 1
by A7, NAT_1:13;
then
lower_bound (divset (MD1,(i + 1))) = MD1 . ((i + 1) - 1)
by A6, INTEGRA1:def 4;
then A11:
lower_bound (divset (MD1,(i + 1))) = lower_bound A
by A1, A9, FINSEQ_1:41;
A12:
MD1 . (i + 1) =
MD1 . (i + (len <*(lower_bound A)*>))
by FINSEQ_1:40
.=
D1 . i
by A1, A4, FINSEQ_1:def 7
;
upper_bound (divset (MD1,(i + 1))) = MD1 . (i + 1)
by A6, A10, INTEGRA1:def 4;
hence
(
lower_bound (divset (D1,i)) = lower_bound (divset (MD1,(i + 1))) &
upper_bound (divset (D1,i)) = upper_bound (divset (MD1,(i + 1))) )
by A4, A9, A11, A12, INTEGRA1:def 4;
verum end; suppose A13:
i <> 1
;
( 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 A7, NAT_1:13;
MD1 . (i + 1) =
MD1 . (i + (len <*(lower_bound A)*>))
by FINSEQ_1:40
.=
D1 . i
by A1, A4, FINSEQ_1:def 7
;
then A15:
upper_bound (divset (MD1,(i + 1))) =
D1 . i
by A6, A14, INTEGRA1:def 4
.=
upper_bound (divset (D1,i))
by A4, A13, INTEGRA1:def 4
;
i - 1
in dom D1
by A4, A13, INTEGRA1:7;
then D1 . (i - 1) =
MD1 . ((i - 1) + (len <*(lower_bound A)*>))
by A1, FINSEQ_1:def 7
.=
MD1 . ((i - 1) + 1)
by FINSEQ_1:39
.=
MD1 . ((i + 1) - 1)
;
then lower_bound (divset (D1,i)) =
MD1 . ((i + 1) - 1)
by A4, A13, INTEGRA1:def 4
.=
lower_bound (divset (MD1,(i + 1)))
by A6, A14, INTEGRA1:def 4
;
hence
(
lower_bound (divset (D1,i)) = lower_bound (divset (MD1,(i + 1))) &
upper_bound (divset (D1,i)) = upper_bound (divset (MD1,(i + 1))) )
by A15;
verum end;
end;
divset (
D1,
i)
= [.(lower_bound (divset (D1,i))),(upper_bound (divset (D1,i))).]
by INTEGRA1:4;
hence
divset (
MD1,
(i + 1))
= divset (
D1,
i)
by A8, INTEGRA1:4;
verum
end;
A16: len MD1 =
(len <*(lower_bound A)*>) + (len D1)
by A1, FINSEQ_1:22
.=
1 + (len D1)
by FINSEQ_1:39
;
thus
upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1
lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1proof
set D2 =
D1;
set MD2 =
MD1;
rng (upper_volume (f,MD1)) <> {}
;
then
1
in dom (upper_volume (f,MD1))
by FINSEQ_3:32;
then
1
<= len (upper_volume (f,MD1))
by FINSEQ_3:25;
then len ((upper_volume (f,MD1)) /^ 1) =
(len (upper_volume (f,MD1))) - 1
by RFINSEQ:def 1
.=
(len MD1) - 1
by INTEGRA1:def 6
.=
len D1
by A16
;
then A17:
len (upper_volume (f,D1)) = len ((upper_volume (f,MD1)) /^ 1)
by INTEGRA1:def 6;
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;
( 1 <= k & k <= len (upper_volume (f,D1)) implies (upper_volume (f,D1)) . k = ((upper_volume (f,MD1)) /^ 1) . k )
assume that A18:
1
<= k
and A19:
k <= len (upper_volume (f,D1))
;
(upper_volume (f,D1)) . k = ((upper_volume (f,MD1)) /^ 1) . k
k + 1
<= (len (upper_volume (f,D1))) + 1
by A19, XREAL_1:6;
then A20:
k + 1
<= (len D1) + 1
by INTEGRA1:def 6;
k in Seg (len (upper_volume (f,D1)))
by A18, A19, FINSEQ_1:1;
then A21:
k in Seg (len D1)
by INTEGRA1:def 6;
then
k in dom D1
by FINSEQ_1:def 3;
then A22:
(upper_volume (f,D1)) . k =
(upper_bound (rng (f | (divset (D1,k))))) * (vol (divset (D1,k)))
by INTEGRA1:def 6
.=
(upper_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (D1,k)))
by A2, A21
.=
(upper_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (MD1,(k + 1))))
by A2, A21
;
A23:
len ((upper_volume (f,MD1)) /^ 1) <= len (upper_volume (f,MD1))
by FINSEQ_5:25;
1
<= k + 1
by NAT_1:11;
then
k + 1
in Seg (len MD1)
by A16, A20, FINSEQ_1:1;
then A24:
k + 1
in dom MD1
by FINSEQ_1:def 3;
1
<= len (upper_volume (f,D1))
by A18, A19, XXREAL_0:2;
then A25:
1
<= len (upper_volume (f,MD1))
by A17, A23, XXREAL_0:2;
k in dom ((upper_volume (f,MD1)) /^ 1)
by A17, A18, A19, FINSEQ_3:25;
then ((upper_volume (f,MD1)) /^ 1) . k =
(upper_volume (f,MD1)) . (k + 1)
by A25, RFINSEQ:def 1
.=
(upper_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (MD1,(k + 1))))
by A24, INTEGRA1:def 6
;
hence
(upper_volume (f,D1)) . k = ((upper_volume (f,MD1)) /^ 1) . k
by A22;
verum
end;
hence
upper_volume (
f,
D1)
= (upper_volume (f,MD1)) /^ 1
by A17, FINSEQ_1:14;
verum
end;
rng (lower_volume (f,MD1)) <> {}
;
then
1 in dom (lower_volume (f,MD1))
by FINSEQ_3:32;
then
1 <= len (lower_volume (f,MD1))
by FINSEQ_3:25;
then len ((lower_volume (f,MD1)) /^ 1) =
(len (lower_volume (f,MD1))) - 1
by RFINSEQ:def 1
.=
(len MD1) - 1
by INTEGRA1:def 7
.=
len D1
by A16
;
then A26:
len (lower_volume (f,D1)) = len ((lower_volume (f,MD1)) /^ 1)
by INTEGRA1:def 7;
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;
( 1 <= k & k <= len (lower_volume (f,D1)) implies (lower_volume (f,D1)) . k = ((lower_volume (f,MD1)) /^ 1) . k )
assume that A27:
1
<= k
and A28:
k <= len (lower_volume (f,D1))
;
(lower_volume (f,D1)) . k = ((lower_volume (f,MD1)) /^ 1) . k
A29:
1
<= k + 1
by NAT_1:11;
k in Seg (len (lower_volume (f,D1)))
by A27, A28, FINSEQ_1:1;
then A30:
k in Seg (len D1)
by INTEGRA1:def 7;
then
k in dom D1
by FINSEQ_1:def 3;
then A31:
(lower_volume (f,D1)) . k =
(lower_bound (rng (f | (divset (D1,k))))) * (vol (divset (D1,k)))
by INTEGRA1:def 7
.=
(lower_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (D1,k)))
by A2, A30
.=
(lower_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (MD1,(k + 1))))
by A2, A30
;
A32:
len ((lower_volume (f,MD1)) /^ 1) <= len (lower_volume (f,MD1))
by FINSEQ_5:25;
k + 1
<= (len (lower_volume (f,D1))) + 1
by A28, XREAL_1:6;
then A33:
k + 1
<= (len D1) + 1
by INTEGRA1:def 7;
len MD1 =
(len <*(lower_bound A)*>) + (len D1)
by A1, FINSEQ_1:22
.=
(len D1) + 1
by FINSEQ_1:39
;
then
k + 1
in Seg (len MD1)
by A29, A33, FINSEQ_1:1;
then A34:
k + 1
in dom MD1
by FINSEQ_1:def 3;
1
<= len ((lower_volume (f,MD1)) /^ 1)
by A26, A27, A28, XXREAL_0:2;
then A35:
1
<= len (lower_volume (f,MD1))
by A32, XXREAL_0:2;
k in dom ((lower_volume (f,MD1)) /^ 1)
by A26, A27, A28, FINSEQ_3:25;
then ((lower_volume (f,MD1)) /^ 1) . k =
(lower_volume (f,MD1)) . (k + 1)
by A35, RFINSEQ:def 1
.=
(lower_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (MD1,(k + 1))))
by A34, INTEGRA1:def 7
;
hence
(lower_volume (f,D1)) . k = ((lower_volume (f,MD1)) /^ 1) . k
by A31;
verum
end;
hence
lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1
by A26, FINSEQ_1:14; verum