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