let I be non empty closed_interval Subset of REAL; 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; ( 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;
( 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
;
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
;
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;
( TD is jauge -fine implies |.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon )
assume
TD is
jauge -fine
;
|.((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
;
verum
end;
hence
for
TD being
tagged_division of
I st
TD is
jauge -fine holds
|.((tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon
;
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
;
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; verum