let I1, I2 be Real; :: thesis: ( ( for T being DivSequence of A

for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum S is convergent & lim (middle_sum S) = I1 ) ) & ( for T being DivSequence of A

for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum S is convergent & lim (middle_sum S) = I2 ) ) implies I1 = I2 )

assume A2: for T being DivSequence of A

for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum S is convergent & lim (middle_sum S) = I1 ) ; :: thesis: ( ex T being DivSequence of A ex S being middle_volume_Sequence of rho,u,T st

( delta T is convergent & lim (delta T) = 0 & not ( middle_sum S is convergent & lim (middle_sum S) = I2 ) ) or I1 = I2 )

assume A3: for T being DivSequence of A

for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum S is convergent & lim (middle_sum S) = I2 ) ; :: thesis: I1 = I2

consider T being DivSequence of A such that

A4: ( delta T is convergent & lim (delta T) = 0 ) by INTEGRA4:11;

set S = the middle_volume_Sequence of rho,u,T;

thus I1 = lim (middle_sum the middle_volume_Sequence of rho,u,T) by A2, A4

.= I2 by A3, A4 ; :: thesis: verum

for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum S is convergent & lim (middle_sum S) = I1 ) ) & ( for T being DivSequence of A

for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum S is convergent & lim (middle_sum S) = I2 ) ) implies I1 = I2 )

assume A2: for T being DivSequence of A

for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum S is convergent & lim (middle_sum S) = I1 ) ; :: thesis: ( ex T being DivSequence of A ex S being middle_volume_Sequence of rho,u,T st

( delta T is convergent & lim (delta T) = 0 & not ( middle_sum S is convergent & lim (middle_sum S) = I2 ) ) or I1 = I2 )

assume A3: for T being DivSequence of A

for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum S is convergent & lim (middle_sum S) = I2 ) ; :: thesis: I1 = I2

consider T being DivSequence of A such that

A4: ( delta T is convergent & lim (delta T) = 0 ) by INTEGRA4:11;

set S = the middle_volume_Sequence of rho,u,T;

thus I1 = lim (middle_sum the middle_volume_Sequence of rho,u,T) by A2, A4

.= I2 by A3, A4 ; :: thesis: verum