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 f = chi (I,I) holds
tagged_sum (f,TD) = vol I
let TD be tagged_division of I; for f being Function of I,REAL st f = chi (I,I) holds
tagged_sum (f,TD) = vol I
let f be Function of I,REAL; ( f = chi (I,I) implies tagged_sum (f,TD) = vol I )
assume A1:
f = chi (I,I)
; tagged_sum (f,TD) = vol I
A2:
for i being Nat st i in dom TD holds
(tagged_volume (f,TD)) . i = vol (divset ((division_of TD),i))
proof
let i be
Nat;
( i in dom TD implies (tagged_volume (f,TD)) . i = vol (divset ((division_of TD),i)) )
assume A3:
i in dom TD
;
(tagged_volume (f,TD)) . i = vol (divset ((division_of TD),i))
consider D being
Division of
I,
T being
Element of
set_of_tagged_Division D such that A4:
tagged_of TD = T
and A5:
TD = [D,T]
by Def2;
A6:
i in dom D
by A3, Th20, A5;
A7:
dom T =
Seg (len (tagged_of TD))
by A4, FINSEQ_1:def 3
.=
Seg (len (division_of TD))
by Th21
.=
Seg (len D)
by A5, Th20
.=
dom D
by FINSEQ_1:def 3
;
rng T c= I
by Th22;
then
T . i in I
by A7, A6, FUNCT_1:3;
then
f . ((tagged_of TD) . i) = 1
by A4, A1, FUNCT_3:def 3;
then (tagged_volume (f,TD)) . i =
1
* (vol (divset ((division_of TD),i)))
by Def4, A3
.=
vol (divset ((division_of TD),i))
;
hence
(tagged_volume (f,TD)) . i = vol (divset ((division_of TD),i))
;
verum
end;
T1: dom (tagged_volume (f,TD)) =
Seg (len (tagged_volume (f,TD)))
by FINSEQ_1:def 3
.=
Seg (len TD)
by Def4
.=
Seg (len (division_of TD))
;
Seg (len (division_of TD)) = dom (division_of TD)
by FINSEQ_1:def 3;
hence
tagged_sum (f,TD) = vol I
by INTEGR20:6, T1, A2; verum