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 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,()
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,()
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,(); :: 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 ;
thus (middle_sum (f,S)) . x = middle_sum (f,(S . n)) by INTEGR15:def 8
.= (middle_sum (g,U)) . x by ; :: thesis: verum
end;
hence middle_sum (f,S) = middle_sum (g,U) by ; :: thesis: verum