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 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; :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( f = g & S = U implies middle_sum (f,S) = middle_sum (g,U) )

assume A1: ( f = g & S = U ) ; :: thesis: 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 ;

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; :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( f = g & S = U implies middle_sum (f,S) = middle_sum (g,U) )

assume A1: ( f = g & S = U ) ; :: thesis: 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 :: thesis: for x being object st x in dom (middle_sum (f,S)) holds

(middle_sum (f,S)) . x = (middle_sum (g,U)) . x

hence
middle_sum (f,S) = middle_sum (g,U)
by A2, FUNCT_1:2; :: thesis: verum(middle_sum (f,S)) . x = (middle_sum (g,U)) . x

let x be object ; :: thesis: ( 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)) ; :: thesis: (middle_sum (f,S)) . x = (middle_sum (g,U)) . x

then 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 ; :: thesis: verum

end;assume x in dom (middle_sum (f,S)) ; :: thesis: (middle_sum (f,S)) . x = (middle_sum (g,U)) . x

then 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 ; :: thesis: verum