let J1, J2 be Real; ( ( 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
; J1 = J2
now for epsilon being Real st epsilon > 0 holds
|.(J1 - J2).| <= epsilonlet epsilon be
Real;
( epsilon > 0 implies |.(J1 - J2).| <= epsilon )assume A4:
epsilon > 0
;
|.(J1 - J2).| <= epsilonreconsider 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
;
verum end;
hence
J1 = J2
by Th04; verum