let I be non empty closed_interval Subset of REAL; :: thesis: for f being bounded integrable Function of I,REAL holds
( f is HK-integrable & HK-integral f = integral f )
let f be bounded integrable Function of I,REAL; :: thesis: ( f is HK-integrable & HK-integral f = integral f )

per cases ( f is constant or not f is constant ) ;

suppose A1: f is constant ; :: thesis: ( f is HK-integrable & HK-integral f = integral f )

then consider r being Real such that
A2: f = r (#) (chi (I,I)) and
A3: HK-integral f = r * (vol I) by Th36;
reconsider g = chi (I,I) as Function of I,REAL by Th11;
A4: g | I is bounded by Th14;
g is integrable by INTEGRA4:2;
then integral f = r * (integral g) by A2, A4, INTEGRA2:31;
hence ( f is HK-integrable & HK-integral f = integral f ) by A1, Th36, A3, INTEGRA4:2; :: thesis: verum

end;

suppose A5: not f is constant ; :: thesis: ( f is HK-integrable & HK-integral f = integral f )

per cases ( I is trivial or not I is trivial ) ;

suppose I is trivial ; :: thesis: ( f is HK-integrable & HK-integral f = integral f )

then ( f is HK-integrable & HK-integral f = 0 & vol I = 0 ) by Th25, Th27;
hence ( f is HK-integrable & HK-integral f = integral f ) by INTEGRA4:6; :: thesis: verum

end;

suppose A6: not I is trivial ; :: thesis: ( f is HK-integrable & HK-integral f = integral f )

set J = integral f;

A7: 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)) - (integral f)).| <= 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)) - (integral f)).| <= epsilon )
assume A8: 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)) - (integral f)).| <= epsilon
consider D being Division of I such that
A9: D . 1 <> lower_bound I and
A10: upper_sum (f,D) < (integral f) + (epsilon / 2) and
A11: (integral f) - (epsilon / 2) < lower_sum (f,D) and
(upper_sum (f,D)) - (lower_sum (f,D)) < epsilon by A6, A8, Th41;
reconsider fc = chi (I,I) as Function of I,REAL by Th11;
0 < min (rng (upper_volume (fc,D)))

proof

assume not 0 < min (rng (upper_volume (fc,D))) ; :: thesis: contradiction
then 0 = min (rng (upper_volume (fc,D))) by Th46;
then divset (D,1) = [.(D . 1),(D . 1).] by Th46;
hence contradiction by A9, Th47; :: thesis: verum

end;

then reconsider r1 = min (rng (upper_volume (fc,D))) as positive Real ;
|.((upper_bound (rng f)) - (lower_bound (rng f))).| <> 0 by A5, Th37;
then reconsider r2 = epsilon / ((2 * (len D)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|) as positive Real by A8;
reconsider s = (min (r1,r2)) / 2 as positive Real ;
chi (I,I) is positive-yielding by Th17;
then reconsider jauge = s (#) fc as positive-yielding Function of I,REAL ;
take jauge = jauge; :: thesis: for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - (integral f)).| <= epsilon
thus for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - (integral f)).| <= epsilon :: thesis: verum

proof

let TD be tagged_division of I; :: thesis: ( TD is jauge -fine implies |.((tagged_sum (f,TD)) - (integral f)).| <= epsilon )
assume A12: TD is jauge -fine ; :: thesis: |.((tagged_sum (f,TD)) - (integral f)).| <= epsilon
( Sum (lower_volume (f,(division_of TD))) <= Sum (tagged_volume (f,TD)) & Sum (tagged_volume (f,TD)) <= Sum (upper_volume (f,(division_of TD))) ) by Th40;
then A13: ( lower_sum (f,(division_of TD)) <= tagged_sum (f,TD) & tagged_sum (f,TD) <= upper_sum (f,(division_of TD)) ) by INTEGRA1:def 8, INTEGRA1:def 9;
A14: ( f | I is bounded & delta (division_of TD) < min (rng (upper_volume (fc,D))) ) by A12, Th44;
then consider D9 being Division of I such that
A15: D <= D9 and
A16: division_of TD <= D9 and
A17: rng D9 = (rng (division_of TD)) \/ (rng D) and
A18: (upper_sum (f,(division_of TD))) - (upper_sum (f,D9)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta (division_of TD)) by INTEGRA3:24;
consider D9B being Division of I such that
D <= D9B and
division_of TD <= D9B and
A19: rng D9B = (rng (division_of TD)) \/ (rng D) and
A20: (lower_sum (f,D9B)) - (lower_sum (f,(division_of TD))) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta (division_of TD)) by A14, INTEGRA3:22;
f | I is bounded_above ;
then A21: ( upper_sum (f,D9) <= upper_sum (f,(division_of TD)) & upper_sum (f,D9) <= upper_sum (f,D) ) by A16, A15, INTEGRA1:45;
f | I is bounded_below ;
then A22: ( lower_sum (f,(division_of TD)) <= lower_sum (f,D9) & lower_sum (f,D) <= lower_sum (f,D9) ) by A16, A15, INTEGRA1:46;
A23: integral f = upper_integral f by INTEGRA1:def 17;
then A24: integral f = lower_integral f by INTEGRA1:def 16;
then A25: lower_sum (f,(division_of TD)) <= integral f by Th18, INTEGRA1:def 16;
A26: ( (integral f) - (epsilon / 2) < lower_sum (f,D9) & lower_sum (f,D9) <= integral f ) by A22, A11, XXREAL_0:2, Th18, INTEGRA1:def 16, A24;
A27: integral f <= upper_sum (f,(division_of TD)) by A23, Th19, INTEGRA1:def 16;
A28: ( integral f <= upper_sum (f,D9) & upper_sum (f,D9) < (integral f) + (epsilon / 2) ) by A21, A10, XXREAL_0:2, A23, INTEGRA1:def 16, Th19;

now :: thesis: ( (upper_sum (f,(division_of TD))) - (upper_sum (f,D9)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta (division_of TD)) & 0 <= len D & 0 <= (upper_bound (rng f)) - (lower_bound (rng f)) & 0 <= delta (division_of TD) & delta (division_of TD) < epsilon / ((2 * (len D)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|) )

thus (upper_sum (f,(division_of TD))) - (upper_sum (f,D9)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta (division_of TD)) by A18; :: thesis: ( 0 <= len D & 0 <= (upper_bound (rng f)) - (lower_bound (rng f)) & 0 <= delta (division_of TD) & delta (division_of TD) < epsilon / ((2 * (len D)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|) )
thus 0 <= len D ; :: thesis: ( 0 <= (upper_bound (rng f)) - (lower_bound (rng f)) & 0 <= delta (division_of TD) & delta (division_of TD) < epsilon / ((2 * (len D)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|) )
lower_bound (rng f) <= upper_bound (rng f) by INTEGRA1:15, SEQ_4:11;
hence 0 <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:48; :: thesis: ( 0 <= delta (division_of TD) & delta (division_of TD) < epsilon / ((2 * (len D)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|) )
thus 0 <= delta (division_of TD) by INTEGRA3:9; :: thesis: delta (division_of TD) < epsilon / ((2 * (len D)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|)
thus delta (division_of TD) < epsilon / ((2 * (len D)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|) by A12, Th44; :: thesis: verum

end;

then A29: (upper_sum (f,(division_of TD))) - (upper_sum (f,D9)) <= epsilon / 2 by Th07;
A30: (lower_sum (f,D9)) - (lower_sum (f,(division_of TD))) <= epsilon / 2

proof

A31: (lower_sum (f,D9)) - (lower_sum (f,(division_of TD))) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta (division_of TD)) by A20, A17, A19, INTEGRA3:6;
lower_bound (rng f) <= upper_bound (rng f) by INTEGRA1:15, SEQ_4:11;
then A32: 0 <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:48;
0 <= delta (division_of TD) by INTEGRA3:9;
hence (lower_sum (f,D9)) - (lower_sum (f,(division_of TD))) <= epsilon / 2 by A31, A32, Th07, A12, Th44; :: thesis: verum

end;

A33: |.((lower_sum (f,(division_of TD))) - (integral f)).| <= epsilon

proof

((integral f) - (epsilon / 2)) - (lower_sum (f,(division_of TD))) <= (lower_sum (f,D9)) - (lower_sum (f,(division_of TD))) by A26, XREAL_1:9;
then ((integral f) - (epsilon / 2)) - (lower_sum (f,(division_of TD))) <= epsilon / 2 by A30, XXREAL_0:2;
then (((integral f) - (lower_sum (f,(division_of TD)))) - (epsilon / 2)) + (epsilon / 2) <= (epsilon / 2) + (epsilon / 2) by XREAL_1:6;
hence |.((lower_sum (f,(division_of TD))) - (integral f)).| <= epsilon by Th01, A25; :: thesis: verum

end;

|.((upper_sum (f,(division_of TD))) - (integral f)).| <= epsilon

proof

(upper_sum (f,(division_of TD))) - ((integral f) + (epsilon / 2)) < (upper_sum (f,(division_of TD))) - (upper_sum (f,D9)) by A28, XREAL_1:15;
then (upper_sum (f,(division_of TD))) - ((integral f) + (epsilon / 2)) < epsilon / 2 by A29, XXREAL_0:2;
then (((upper_sum (f,(division_of TD))) - (integral f)) - (epsilon / 2)) + (epsilon / 2) < (epsilon / 2) + (epsilon / 2) by XREAL_1:8;
hence |.((upper_sum (f,(division_of TD))) - (integral f)).| <= epsilon by A27, Th02; :: thesis: verum

end;

hence |.((tagged_sum (f,TD)) - (integral f)).| <= epsilon by A13, A33, Th03; :: thesis: verum

end;

end;

hence f is HK-integrable ; :: thesis: HK-integral f = integral f
hence HK-integral f = integral f by A7, DEFCC; :: thesis: verum

end;

end;

end;

end;