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 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,()
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,()
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,(); :: 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 ; :: thesis: verum