let I be non empty closed_interval Subset of REAL; :: thesis: for TD being tagged_division of I
for f, g being HK-integrable Function of I,REAL
for i being Nat st i in dom TD holds
(tagged_volume ((f + g),TD)) . i = ((f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) + ((g . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))))
let TD be tagged_division of I; :: thesis: for f, g being HK-integrable Function of I,REAL
for i being Nat st i in dom TD holds
(tagged_volume ((f + g),TD)) . i = ((f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) + ((g . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))))
let f, g be HK-integrable Function of I,REAL; :: thesis: for i being Nat st i in dom TD holds
(tagged_volume ((f + g),TD)) . i = ((f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) + ((g . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))))
let i be Nat; :: thesis: ( i in dom TD implies (tagged_volume ((f + g),TD)) . i = ((f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) + ((g . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) )
assume A1: i in dom TD ; :: thesis: (tagged_volume ((f + g),TD)) . i = ((f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) + ((g . ((tagged_of 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
A2: tagged_of TD = T and
A3: TD = [D,T] by Def2;
A4: i in dom D by A1, Th20, A3;
A5: dom T = Seg (len (tagged_of TD)) by A2, FINSEQ_1:def 3
.= Seg (len (division_of TD)) by Th21
.= Seg (len D) by A3, Th20
.= dom D by FINSEQ_1:def 3 ;
rng T c= I by Th22;
then reconsider c = (tagged_of TD) . i as Element of I by A2, A4, A5, FUNCT_1:3;
(tagged_volume ((f + g),TD)) . i = ((f + g) . c) * (vol (divset ((division_of TD),i))) by A1, Def4
.= ((f . c) + (g . c)) * (vol (divset ((division_of TD),i))) by VALUED_1:1 ;
hence (tagged_volume ((f + g),TD)) . i = ((f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) + ((g . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) ; :: thesis: verum