let I be non empty closed_interval Subset of REAL; :: thesis: for f being Function of I,REAL st I is trivial holds
( f is HK-integrable & HK-integral f = 0 )
let f be Function of I,REAL; :: thesis: ( I is trivial implies ( f is HK-integrable & HK-integral f = 0 ) )
assume A1: I is trivial ; :: thesis: ( f is HK-integrable & HK-integral f = 0 )
reconsider J = 0 as Real ;
A2: now :: thesis: 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)) - J).| <= epsilon
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,TD)) - J).| <= epsilon )
assume A3: 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,TD)) - J).| <= epsilon
reconsider jauge = chi (I,I) as positive-yielding Function of I,REAL by Th17, Th11;
take jauge = jauge; :: thesis: for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - J).| <= epsilon
thus for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - J).| <= epsilon :: thesis: verum
proof
let TD be tagged_division of I; :: thesis: ( TD is jauge -fine implies |.((tagged_sum (f,TD)) - J).| <= epsilon )
assume TD is jauge -fine ; :: thesis: |.((tagged_sum (f,TD)) - J).| <= epsilon
consider x being object such that
A4: I = {x} by A1, ZFMISC_1:131;
x in I by A4, TARSKI:def 1;
then reconsider x = x as Real ;
A4Bis: division_of TD = <*x*> by A4, Th26;
A5: ( len (tagged_volume (f,TD)) = len TD & ( for i being Nat st i in dom TD holds
(tagged_volume (f,TD)) . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) ) by Def4;
A6: (tagged_volume (f,TD)) . 1 = (f . ((tagged_of TD) . 1)) * (vol (divset ((division_of TD),1))) by A5, FINSEQ_5:6;
divset ((division_of TD),1) = [.(lower_bound I),((division_of TD) . 1).] by COUSIN:50
.= [.x,((division_of TD) . 1).] by A4, SEQ_4:9
.= [.x,x.] by A4Bis, FINSEQ_1:40
.= {x} by XXREAL_1:17 ;
then A7: vol (divset ((division_of TD),1)) = 0 by COUSIN:41;
len (tagged_volume (f,TD)) = len TD by Def4
.= 1 by A4Bis, FINSEQ_1:40 ;
then tagged_volume (f,TD) = <*((tagged_volume (f,TD)) . 1)*> by FINSEQ_1:40;
then Sum (tagged_volume (f,TD)) = 0 by A6, A7, RVSUM_1:73;
hence |.((tagged_sum (f,TD)) - J).| <= epsilon by A3; :: thesis: verum
end;
end;
then f is HK-integrable ;
hence ( f is HK-integrable & HK-integral f = 0 ) by A2, DEFCC; :: thesis: verum