let A be Subset of REAL; for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being Function of I,REAL st A misses I & f = chi (A,I) holds
tagged_sum (f,TD) = 0
let I be non empty closed_interval Subset of REAL; for TD being tagged_division of I
for f being Function of I,REAL st A misses I & f = chi (A,I) holds
tagged_sum (f,TD) = 0
let TD be tagged_division of I; for f being Function of I,REAL st A misses I & f = chi (A,I) holds
tagged_sum (f,TD) = 0
let f be Function of I,REAL; ( A misses I & f = chi (A,I) implies tagged_sum (f,TD) = 0 )
assume that
A1:
A misses I
and
A2:
f = chi (A,I)
; tagged_sum (f,TD) = 0
A3: dom (tagged_volume (f,TD)) =
Seg (len (tagged_volume (f,TD)))
by FINSEQ_1:def 3
.=
Seg (len TD)
by Def4
.=
dom TD
by FINSEQ_1:def 3
;
for i being Nat st i in dom TD holds
(tagged_volume (f,TD)) . i = 0
proof
let i be
Nat;
( i in dom TD implies (tagged_volume (f,TD)) . i = 0 )
assume A4:
i in dom TD
;
(tagged_volume (f,TD)) . i = 0
consider D being
Division of
I,
T being
Element of
set_of_tagged_Division D such that A5:
tagged_of TD = T
and A6:
TD = [D,T]
by Def2;
A7:
i in dom D
by A4, Th20, A6;
A8:
dom T =
Seg (len (tagged_of TD))
by A5, FINSEQ_1:def 3
.=
Seg (len (division_of TD))
by Th21
.=
Seg (len D)
by A6, Th20
.=
dom D
by FINSEQ_1:def 3
;
rng T c= I
by Th22;
then
T . i in I
by A8, A7, FUNCT_1:3;
then
f . ((tagged_of TD) . i) = 0
by A1, A5, A2, Th15;
then (tagged_volume (f,TD)) . i =
0 * (vol (divset ((division_of TD),i)))
by Def4, A4
.=
0
;
hence
(tagged_volume (f,TD)) . i = 0
;
verum
end;
then
for k being object st k in dom (tagged_volume (f,TD)) holds
(tagged_volume (f,TD)) . k = 0
by A3;
then Sum (tagged_volume (f,TD)) =
Sum ((len (tagged_volume (f,TD))) |-> 0)
by INTEGR23:5
.=
0
by RVSUM_1:81
;
hence
tagged_sum (f,TD) = 0
; verum