let A be Subset of REAL; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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; :: thesis: ( i in dom TD implies (tagged_volume (f,TD)) . i = 0 )
assume A4: i in dom TD ; :: thesis: (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 ; :: thesis: 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 ; :: thesis: verum