let n be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

for g being Function of A,(REAL-NS n)

for I being Element of REAL n

for J being Point of (REAL-NS n) st f = g & I = J holds

( ( 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,(REAL n)

for g being Function of A,(REAL-NS n)

for I being Element of REAL n

for J being Point of (REAL-NS n) st f = g & I = J holds

( ( 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

let f be Function of A,(REAL n); :: thesis: for g being Function of A,(REAL-NS n)

for I being Element of REAL n

for J being Point of (REAL-NS n) st f = g & I = J holds

( ( 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

let g be Function of A,(REAL-NS n); :: thesis: for I being Element of REAL n

for J being Point of (REAL-NS n) st f = g & I = J holds

( ( 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

let I be Element of REAL n; :: thesis: for J being Point of (REAL-NS n) st f = g & I = J holds

( ( 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

let J be Point of (REAL-NS n); :: thesis: ( f = g & I = J implies ( ( 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) )

assume A1: ( f = g & I = J ) ; :: 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ; :: 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)) = I )

A6: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;

thus for T being DivSequence of A

for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) :: thesis: verum

for f being Function of A,(REAL n)

for g being Function of A,(REAL-NS n)

for I being Element of REAL n

for J being Point of (REAL-NS n) st f = g & I = J holds

( ( 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,(REAL n)

for g being Function of A,(REAL-NS n)

for I being Element of REAL n

for J being Point of (REAL-NS n) st f = g & I = J holds

( ( 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

let f be Function of A,(REAL n); :: thesis: for g being Function of A,(REAL-NS n)

for I being Element of REAL n

for J being Point of (REAL-NS n) st f = g & I = J holds

( ( 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

let g be Function of A,(REAL-NS n); :: thesis: for I being Element of REAL n

for J being Point of (REAL-NS n) st f = g & I = J holds

( ( 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

let I be Element of REAL n; :: thesis: for J being Point of (REAL-NS n) st f = g & I = J holds

( ( 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

let J be Point of (REAL-NS n); :: thesis: ( f = g & I = J implies ( ( 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) )

assume A1: ( f = g & I = J ) ; :: 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)) = I ) ) iff for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

hereby :: thesis: ( ( for T being DivSequence of A

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) implies 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)) = I ) )

assume A5:
for T being DivSequence of Afor S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) implies 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)) = I ) )

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)) = I ) ; :: thesis: for T being DivSequence of A

for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )

A3: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;

thus for T being DivSequence of A

for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) :: thesis: verum

end;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)) = I ) ; :: thesis: for T being DivSequence of A

for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )

A3: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;

thus for T being DivSequence of A

for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) :: thesis: verum

proof

let T be DivSequence of A; :: thesis: for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )

let S0 be middle_volume_Sequence of g,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) )

assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )

reconsider S = S0 as middle_volume_Sequence of f,T by A3, A1, Th38;

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A2, A4;

hence ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) by A1, Th39; :: thesis: verum

end;( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )

let S0 be middle_volume_Sequence of g,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) )

assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )

reconsider S = S0 as middle_volume_Sequence of f,T by A3, A1, Th38;

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A2, A4;

hence ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) by A1, Th39; :: thesis: verum

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

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ; :: 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)) = I )

A6: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;

thus for T being DivSequence of A

for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) :: thesis: verum

proof

let T be DivSequence of A; :: thesis: for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I )

let S0 be middle_volume_Sequence of f,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) )

assume A7: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I )

reconsider S = S0 as middle_volume_Sequence of g,T by A6, A1, Th38;

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = I ) by A1, A5, A7;

hence ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) by A1, Th39; :: thesis: verum

end;( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I )

let S0 be middle_volume_Sequence of f,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) )

assume A7: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I )

reconsider S = S0 as middle_volume_Sequence of g,T by A6, A1, Th38;

( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = I ) by A1, A5, A7;

hence ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) by A1, Th39; :: thesis: verum