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 FinSequence of REAL n

for q being FinSequence of (REAL-NS n) st f = g & p = q holds

( p is middle_volume of f,D iff q is middle_volume of g,D )

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 FinSequence of REAL n

for q being FinSequence of (REAL-NS n) st f = g & p = q holds

( p is middle_volume of f,D iff q is middle_volume of g,D )

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 FinSequence of REAL n

for q being FinSequence of (REAL-NS n) st f = g & p = q holds

( p is middle_volume of f,D iff q is middle_volume of g,D )

let g be Function of A,(REAL-NS n); :: thesis: for D being Division of A

for p being FinSequence of REAL n

for q being FinSequence of (REAL-NS n) st f = g & p = q holds

( p is middle_volume of f,D iff q is middle_volume of g,D )

let D be Division of A; :: thesis: for p being FinSequence of REAL n

for q being FinSequence of (REAL-NS n) st f = g & p = q holds

( p is middle_volume of f,D iff q is middle_volume of g,D )

let p be FinSequence of REAL n; :: thesis: for q being FinSequence of (REAL-NS n) st f = g & p = q holds

( p is middle_volume of f,D iff q is middle_volume of g,D )

let q be FinSequence of (REAL-NS n); :: thesis: ( f = g & p = q implies ( p is middle_volume of f,D iff q is middle_volume of g,D ) )

assume A1: ( f = g & p = q ) ; :: thesis: ( p is middle_volume of f,D iff q is middle_volume of g,D )

thus ( p is middle_volume of f,D implies q is middle_volume of g,D ) :: thesis: ( q is middle_volume of g,D implies p is middle_volume of f,D )

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 FinSequence of REAL n

for q being FinSequence of (REAL-NS n) st f = g & p = q holds

( p is middle_volume of f,D iff q is middle_volume of g,D )

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 FinSequence of REAL n

for q being FinSequence of (REAL-NS n) st f = g & p = q holds

( p is middle_volume of f,D iff q is middle_volume of g,D )

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 FinSequence of REAL n

for q being FinSequence of (REAL-NS n) st f = g & p = q holds

( p is middle_volume of f,D iff q is middle_volume of g,D )

let g be Function of A,(REAL-NS n); :: thesis: for D being Division of A

for p being FinSequence of REAL n

for q being FinSequence of (REAL-NS n) st f = g & p = q holds

( p is middle_volume of f,D iff q is middle_volume of g,D )

let D be Division of A; :: thesis: for p being FinSequence of REAL n

for q being FinSequence of (REAL-NS n) st f = g & p = q holds

( p is middle_volume of f,D iff q is middle_volume of g,D )

let p be FinSequence of REAL n; :: thesis: for q being FinSequence of (REAL-NS n) st f = g & p = q holds

( p is middle_volume of f,D iff q is middle_volume of g,D )

let q be FinSequence of (REAL-NS n); :: thesis: ( f = g & p = q implies ( p is middle_volume of f,D iff q is middle_volume of g,D ) )

assume A1: ( f = g & p = q ) ; :: thesis: ( p is middle_volume of f,D iff q is middle_volume of g,D )

thus ( p is middle_volume of f,D implies q is middle_volume of g,D ) :: thesis: ( q is middle_volume of g,D implies p is middle_volume of f,D )

proof

thus
( q is middle_volume of g,D implies p is middle_volume of f,D )
:: thesis: verum
assume A2:
p is middle_volume of f,D
; :: thesis: q is middle_volume of g,D

then A3: len q = len D by A1, INTEGR15:def 5;

for i being Nat st i in dom D holds

ex c being Point of (REAL-NS n) st

( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c )

end;then A3: len q = len D by A1, INTEGR15:def 5;

for i being Nat st i in dom D holds

ex c being Point of (REAL-NS n) st

( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c )

proof

hence
q is middle_volume of g,D
by A3, INTEGR18:def 1; :: thesis: verum
let i be Nat; :: thesis: ( i in dom D implies ex c being Point of (REAL-NS n) st

( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) )

assume i in dom D ; :: thesis: ex c being Point of (REAL-NS n) st

( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c )

then consider r being Element of REAL n such that

A4: ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) by A2, INTEGR15:def 5;

reconsider c = r as Point of (REAL-NS n) by REAL_NS1:def 4;

take c ; :: thesis: ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c )

thus ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) by A4, A1, REAL_NS1:3; :: thesis: verum

end;( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) )

assume i in dom D ; :: thesis: ex c being Point of (REAL-NS n) st

( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c )

then consider r being Element of REAL n such that

A4: ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) by A2, INTEGR15:def 5;

reconsider c = r as Point of (REAL-NS n) by REAL_NS1:def 4;

take c ; :: thesis: ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c )

thus ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) by A4, A1, REAL_NS1:3; :: thesis: verum

proof

assume A5:
q is middle_volume of g,D
; :: thesis: p is middle_volume of f,D

then A6: len p = len D by A1, INTEGR18:def 1;

for i being Nat st i in dom D holds

ex r being Element of REAL n st

( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r )

end;then A6: len p = len D by A1, INTEGR18:def 1;

for i being Nat st i in dom D holds

ex r being Element of REAL n st

( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r )

proof

hence
p is middle_volume of f,D
by A6, INTEGR15:def 5; :: thesis: verum
let i be Nat; :: thesis: ( i in dom D implies ex r being Element of REAL n st

( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) )

assume A7: i in dom D ; :: thesis: ex r being Element of REAL n st

( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r )

consider c being Point of (REAL-NS n) such that

A8: ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) by A5, A7, INTEGR18:def 1;

reconsider r = c as Element of REAL n by REAL_NS1:def 4;

take r ; :: thesis: ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r )

thus ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) by A8, A1, REAL_NS1:3; :: thesis: verum

end;( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) )

assume A7: i in dom D ; :: thesis: ex r being Element of REAL n st

( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r )

consider c being Point of (REAL-NS n) such that

A8: ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) by A5, A7, INTEGR18:def 1;

reconsider r = c as Element of REAL n by REAL_NS1:def 4;

take r ; :: thesis: ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r )

thus ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) by A8, A1, REAL_NS1:3; :: thesis: verum