let J1, J2 be Real; :: 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)) - J1).| <= epsilon ) & ( 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)) - J2).| <= epsilon ) implies J1 = J2 )
assume that
A2: 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)) - J1).| <= epsilon and
A3: 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)) - J2).| <= epsilon ; :: thesis: J1 = J2

now :: thesis: for epsilon being Real st epsilon > 0 holds
|.(J1 - J2).| <= epsilon

let epsilon be Real; :: thesis: ( epsilon > 0 implies |.(J1 - J2).| <= epsilon )
assume A4: epsilon > 0 ; :: thesis: |.(J1 - J2).| <= epsilon
reconsider e = epsilon / 2 as Real ;
consider jauge1 being positive-yielding Function of I,REAL such that
A5: for TD being tagged_division of I st TD is jauge1 -fine holds
|.((tagged_sum (f,TD)) - J1).| <= e by A4, A2;
consider jauge2 being positive-yielding Function of I,REAL such that
A6: for TD being tagged_division of I st TD is jauge2 -fine holds
|.((tagged_sum (f,TD)) - J2).| <= e by A3, A4;
reconsider jauge = min (jauge1,jauge2) as positive-yielding Function of I,REAL ;
consider TD being tagged_division of I such that
A7: TD is jauge -fine by COUSIN:68;
( TD is jauge1 -fine & TD is jauge2 -fine ) by A7, Th23, Th08;
then ( |.((tagged_sum (f,TD)) - J1).| <= e & |.((tagged_sum (f,TD)) - J2).| <= e ) by A5, A6;
then A8: ( |.(J1 - (tagged_sum (f,TD))).| <= e & |.(J2 - (tagged_sum (f,TD))).| <= e ) by COMPLEX1:60;
|.((J1 - (tagged_sum (f,TD))) - (J2 - (tagged_sum (f,TD)))).| <= |.(J1 - (tagged_sum (f,TD))).| + |.(J2 - (tagged_sum (f,TD))).| by COMPLEX1:57;
then |.(J1 - J2).| <= e + |.(J2 - (tagged_sum (f,TD))).| by A8, Lm01;
then |.(J1 - J2).| <= e + e by A8, Lm01;
hence |.(J1 - J2).| <= epsilon ; :: thesis: verum

end;

hence J1 = J2 by Th04; :: thesis: verum