let I1, I2 be Real; ( ( 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 )
; ( 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 )
; 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
; verum