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 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; for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
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); for g being Function of A,(REAL-NS n)
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,(REAL-NS n); 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; 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; 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; ( f = g & S = U implies middle_sum (f,S) = middle_sum (g,U) )
assume A1:
( f = g & S = U )
; 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 for x being object st x in dom (middle_sum (f,S)) holds
(middle_sum (f,S)) . x = (middle_sum (g,U)) . xlet x be
object ;
( 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))
;
(middle_sum (f,S)) . x = (middle_sum (g,U)) . xthen reconsider n =
x as
Element of
NAT ;
A3:
middle_sum (
f,
(S . n))
= middle_sum (
g,
(U . n))
by A1, Th37;
thus (middle_sum (f,S)) . x =
middle_sum (
f,
(S . n))
by INTEGR15:def 8
.=
(middle_sum (g,U)) . x
by A3, INTEGR18:def 4
;
verum end;
hence
middle_sum (f,S) = middle_sum (g,U)
by A2, FUNCT_1:2; verum