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 T being DivSequence of A
for S being middle_volume_Sequence of f,T
for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
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 T being DivSequence of A
for S being middle_volume_Sequence of f,T
for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
let f be Function of A,(REAL n); :: thesis: for g being Function of A,(REAL-NS n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
let g be Function of A,(REAL-NS n); :: thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of f,T
for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
let S be middle_volume_Sequence of f,T; :: thesis: for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
let U be middle_volume_Sequence of g,T; :: thesis: ( f = g & S = U implies middle_sum (f,S) = middle_sum (g,U) )
assume A1: ( f = g & S = U ) ; :: thesis: middle_sum (f,S) = middle_sum (g,U)
A2: dom (middle_sum (f,S)) = NAT by FUNCT_2:def 1
.= dom (middle_sum (g,U)) by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom (middle_sum (f,S)) holds
(middle_sum (f,S)) . x = (middle_sum (g,U)) . x

let x be object ; :: thesis: ( x in dom (middle_sum (f,S)) implies (middle_sum (f,S)) . x = (middle_sum (g,U)) . x )
assume x in dom (middle_sum (f,S)) ; :: thesis: (middle_sum (f,S)) . x = (middle_sum (g,U)) . x
then reconsider n = x as Element of NAT ;
A3: middle_sum (f,(S . n)) = middle_sum (g,(U . n)) by A1, Th37;
thus (middle_sum (f,S)) . x = middle_sum (f,(S . n)) by INTEGR15:def 8
.= (middle_sum (g,U)) . x by A3, INTEGR18:def 4 ; :: thesis: verum

end;

hence middle_sum (f,S) = middle_sum (g,U) by A2, FUNCT_1:2; :: thesis: verum