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 )

proof

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 )

proof

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;

hence q is middle_volume of g,D by A3, INTEGR18:def 1; :: thesis: verum

end;

thus ( q is middle_volume of g,D implies p is middle_volume of f,D ) :: 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 )

proof

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;

hence p is middle_volume of f,D by A6, INTEGR15:def 5; :: thesis: verum

end;