let n be Element of NAT ; :: thesis:
let A be non empty closed_interval Subset of REAL; :: thesis:
let f be Function of A,(REAL n); :: thesis:
let g be Function of A,(REAL-NS n); :: thesis:
let I be Element of REAL n; :: thesis:
let J be Point of (REAL-NS n); :: thesis:
assume A1: ( f = g & I = J ) ; :: thesis:

hereby :: thesis:

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:
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:

let T be DivSequence of A; :: thesis:
let S0 be middle_volume_Sequence of g,T; :: thesis:
assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis:
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:

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 (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ; :: thesis:
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:

let T be DivSequence of A; :: thesis:
let S0 be middle_volume_Sequence of f,T; :: thesis:
assume A7: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis:
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:

end;