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 D being Division of A

for p being middle_volume of f,D

for q being middle_volume of g,D st f = g & p = q holds

middle_sum (f,p) = middle_sum (g,q)

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 D being Division of A

for p being middle_volume of f,D

for q being middle_volume of g,D st f = g & p = q holds

middle_sum (f,p) = middle_sum (g,q)

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

for D being Division of A

for p being middle_volume of f,D

for q being middle_volume of g,D st f = g & p = q holds

middle_sum (f,p) = middle_sum (g,q)

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

for p being middle_volume of f,D

for q being middle_volume of g,D st f = g & p = q holds

middle_sum (f,p) = middle_sum (g,q)

let D be Division of A; :: thesis: for p being middle_volume of f,D

for q being middle_volume of g,D st f = g & p = q holds

middle_sum (f,p) = middle_sum (g,q)

let p be middle_volume of f,D; :: thesis: for q being middle_volume of g,D st f = g & p = q holds

middle_sum (f,p) = middle_sum (g,q)

let q be middle_volume of g,D; :: thesis: ( f = g & p = q implies middle_sum (f,p) = middle_sum (g,q) )

assume A1: ( f = g & p = q ) ; :: thesis: middle_sum (f,p) = middle_sum (g,q)

for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * p & (middle_sum (f,p)) . i = Sum Pi ) by INTEGR15:def 6;

hence middle_sum (f,p) = middle_sum (g,q) by Lm16, A1; :: thesis: verum

for f being Function of A,(REAL n)

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

for D being Division of A

for p being middle_volume of f,D

for q being middle_volume of g,D st f = g & p = q holds

middle_sum (f,p) = middle_sum (g,q)

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 D being Division of A

for p being middle_volume of f,D

for q being middle_volume of g,D st f = g & p = q holds

middle_sum (f,p) = middle_sum (g,q)

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

for D being Division of A

for p being middle_volume of f,D

for q being middle_volume of g,D st f = g & p = q holds

middle_sum (f,p) = middle_sum (g,q)

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

for p being middle_volume of f,D

for q being middle_volume of g,D st f = g & p = q holds

middle_sum (f,p) = middle_sum (g,q)

let D be Division of A; :: thesis: for p being middle_volume of f,D

for q being middle_volume of g,D st f = g & p = q holds

middle_sum (f,p) = middle_sum (g,q)

let p be middle_volume of f,D; :: thesis: for q being middle_volume of g,D st f = g & p = q holds

middle_sum (f,p) = middle_sum (g,q)

let q be middle_volume of g,D; :: thesis: ( f = g & p = q implies middle_sum (f,p) = middle_sum (g,q) )

assume A1: ( f = g & p = q ) ; :: thesis: middle_sum (f,p) = middle_sum (g,q)

for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * p & (middle_sum (f,p)) . i = Sum Pi ) by INTEGR15:def 6;

hence middle_sum (f,p) = middle_sum (g,q) by Lm16, A1; :: thesis: verum