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,()
for D being Division of A
for p being FinSequence of REAL n
for q being FinSequence of () 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,()
for D being Division of A
for p being FinSequence of REAL n
for q being FinSequence of () 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,()
for D being Division of A
for p being FinSequence of REAL n
for q being FinSequence of () 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,(); :: thesis: for D being Division of A
for p being FinSequence of REAL n
for q being FinSequence of () 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 () 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 () 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 (); :: 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 ;
for i being Nat st i in dom D holds
ex c being Point of () 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 () 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 () 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 ;
reconsider c = r as Point of () 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 ; :: thesis: verum
end;
hence q is middle_volume of g,D by ; :: 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 ;
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 () such that
A8: ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) by ;
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 ; :: thesis: verum
end;
hence p is middle_volume of f,D by ; :: thesis: verum
end;