let I1, I2 be Point of X; :: thesis: ( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I1 ) ) & ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I2 ) ) implies I1 = I2 )
assume A1: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I1 ) ; :: thesis: ( ex T being DivSequence of A ex S being middle_volume_Sequence of f,T st
( delta T is convergent & lim (delta T) = 0 & not ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I2 ) ) or I1 = I2 )
assume A2: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I2 ) ; :: thesis: I1 = I2
consider T being DivSequence of A such that
A3: ( delta T is convergent & lim (delta T) = 0 ) by INTEGRA4:11;
consider S being middle_volume_Sequence of f,T;
thus I1 = lim (middle_sum (f,S)) by A1, A3
.= I2 by A2, A3 ; :: thesis: verum