let A be Subset of REAL; :: thesis:
let I be non empty closed_interval Subset of REAL; :: thesis:
let f be Function of I,REAL; :: thesis:
assume that
A1: A misses I and
A2: f = chi (A,I) ; :: thesis:
reconsider J = 0 as Real ;

A3: now :: thesis:

let epsilon be Real; :: thesis:
assume A4: epsilon > 0 ; :: thesis:
reconsider jauge = chi (I,I) as Function of I,REAL by Th11;

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

end;

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

take jauge = jauge; :: thesis:

hereby :: thesis:

let TD be tagged_division of I; :: thesis:
assume TD is jauge -fine ; :: thesis:
|.((tagged_sum (f,TD)) - J).| = |.0.| by A1, A2, Th28
.= 0 ;
hence |.((tagged_sum (f,TD)) - J).| <= epsilon by A4; :: thesis:

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:

end;

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