let I be non empty closed_interval Subset of REAL; :: thesis: for f, g being HK-integrable Function of I,REAL holds
( f + g is HK-integrable Function of I,REAL & HK-integral (f + g) = (HK-integral f) + (HK-integral g) )
let f, g be HK-integrable Function of I,REAL; :: thesis: ( f + g is HK-integrable Function of I,REAL & HK-integral (f + g) = (HK-integral f) + (HK-integral g) )
f is HK-integrable ;
then consider J1 being Real such that
A1: for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - J1).| <= epsilon ;
g is HK-integrable ;
then consider J2 being Real such that
A2: for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (g,TD)) - J2).| <= epsilon ;
A3: HK-integral g = J2 by A2, DEFCC;
A4: for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon

proof

let epsilon be Real; :: thesis: ( epsilon > 0 implies ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon )
assume A5: epsilon > 0 ; :: thesis: ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon
set e = epsilon / 2;
consider jauge1 being positive-yielding Function of I,REAL such that
A6: for TD being tagged_division of I st TD is jauge1 -fine holds
|.((tagged_sum (f,TD)) - J1).| <= epsilon / 2 by A5, A1;
consider jauge2 being positive-yielding Function of I,REAL such that
A7: for TD being tagged_division of I st TD is jauge2 -fine holds
|.((tagged_sum (g,TD)) - J2).| <= epsilon / 2 by A5, A2;
reconsider jauge = min (jauge1,jauge2) as positive-yielding Function of I,REAL ;
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon

proof

take jauge ; :: thesis: for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon

proof

let TD be tagged_division of I; :: thesis: ( TD is jauge -fine implies |.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon )
assume TD is jauge -fine ; :: thesis: |.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon
then A8: ( TD is jauge1 -fine & TD is jauge2 -fine ) by Th23, Th08;
( len (tagged_volume (f,TD)) = len TD & len (tagged_volume (g,TD)) = len TD ) by Def4;
then reconsider R1 = tagged_volume (f,TD), R2 = tagged_volume (g,TD) as Element of (len TD) -tuples_on REAL by FINSEQ_2:92;
tagged_sum ((f + g),TD) = Sum ((tagged_volume (f,TD)) + (tagged_volume (g,TD))) by Th34
.= (Sum R1) + (Sum R2) by RVSUM_1:89
.= (tagged_sum (f,TD)) + (tagged_sum (g,TD)) ;
then (tagged_sum ((f + g),TD)) - (J1 + J2) = ((tagged_sum (f,TD)) - J1) + ((tagged_sum (g,TD)) - J2) ;
then |.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= |.((tagged_sum (f,TD)) - J1).| + |.((tagged_sum (g,TD)) - J2).| by COMPLEX1:56;
then |.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= (epsilon / 2) + |.((tagged_sum (g,TD)) - J2).| by A8, A6, Lm01;
then |.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= (epsilon / 2) + (epsilon / 2) by A8, A7, Lm01;
hence |.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon ; :: thesis: verum

end;

hence for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon ; :: thesis: verum

end;

hence ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon ; :: thesis: verum

end;

then A9: f + g is HK-integrable ;
then HK-integral (f + g) = J1 + J2 by A4, DEFCC
.= (HK-integral f) + (HK-integral g) by A1, DEFCC, A3 ;
hence ( f + g is HK-integrable Function of I,REAL & HK-integral (f + g) = (HK-integral f) + (HK-integral g) ) by A9; :: thesis: verum