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 f = chi (I,I) holds
tagged_sum (f,TD) = vol I
let TD be tagged_division of I; :: thesis: 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; :: thesis: ( f = chi (I,I) implies tagged_sum (f,TD) = vol I )
assume A1: f = chi (I,I) ; :: thesis: 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; :: thesis: ( i in dom TD implies (tagged_volume (f,TD)) . i = vol (divset ((division_of TD),i)) )
assume A3: i in dom TD ; :: thesis: (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)) ; :: thesis: 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; :: thesis: verum