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,()
for I being Element of REAL n
for J being Point of () 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 () = 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 () = 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,()
for I being Element of REAL n
for J being Point of () 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 () = 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 () = 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,()
for I being Element of REAL n
for J being Point of () 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 () = 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 () = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

let g be Function of A,(); :: thesis: for I being Element of REAL n
for J being Point of () 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 () = 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 () = 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 () 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 () = 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 () = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )

let J be Point of (); :: 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 () = 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 () = 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 () = 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 () = 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 () = 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 () = 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 () = 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 () = 0 holds
( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )

A3: the carrier of () = 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 () = 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 () = 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 () = 0 implies ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) )
assume A4: ( delta T is convergent & lim () = 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 ; :: thesis: verum
end;
end;
assume A5: for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim () = 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 () = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )

A6: the carrier of () = 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 () = 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 () = 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 () = 0 implies ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) )
assume A7: ( delta T is convergent & lim () = 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 ; :: thesis: verum
end;