let A be Subset of REAL; :: thesis: for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st A misses I & f = chi (A,I) holds
( f is HK-integrable & HK-integral f = 0 )
let I be non empty closed_interval Subset of REAL; :: thesis: for f being Function of I,REAL st A misses I & f = chi (A,I) holds
( f is HK-integrable & HK-integral f = 0 )
let f be Function of I,REAL; :: thesis: ( A misses I & f = chi (A,I) implies ( f is HK-integrable & HK-integral f = 0 ) )
assume that
A1: A misses I and
A2: f = chi (A,I) ; :: thesis: ( f is HK-integrable & HK-integral f = 0 )
reconsider J = 0 as Real ;

A3: 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 A4: 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 Function of I,REAL by Th11;

now :: thesis: for r being Real st r in rng jauge holds
0 < r

let r be Real; :: thesis: ( r in rng jauge implies 0 < r )
assume r in rng jauge ; :: thesis: 0 < r
then r in {1} by INTEGRA1:17;
hence 0 < r ; :: thesis: verum

end;

then reconsider jauge = jauge as positive-yielding Function of I,REAL by PARTFUN3:def 1;

now :: 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

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

hereby :: thesis: verum

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
|.((tagged_sum (f,TD)) - J).| = |.0.| by A1, A2, Th28
.= 0 ;
hence |.((tagged_sum (f,TD)) - J).| <= epsilon by A4; :: thesis: verum

end;

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,TD)) - J).| <= epsilon ; :: thesis: verum

end;

then f is HK-integrable ;
hence ( f is HK-integrable & HK-integral f = 0 ) by A3, DEFCC; :: thesis: verum