let n be Element of NAT ; 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; 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); 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); 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; 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; 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; ( f = g & p = q implies middle_sum (f,p) = middle_sum (g,q) )
assume A1:
( f = g & p = q )
; 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; verum