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: I c= A and
A2: f = chi (A,I) ; :: thesis:
reconsider J = vol I 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;

now :: thesis:

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;

now :: thesis:

take jauge = jauge; :: thesis:

hereby :: thesis:

let TD be tagged_division of I; :: thesis:
assume TD is jauge -fine ; :: thesis:
f = chi (I,I) by A1, A2, Th24;
then tagged_sum (f,TD) = vol I by Lm04;
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 = vol I ) by A3, DEFCC; :: thesis: