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 T being DivSequence of A
for p being sequence of ((REAL n) *)
for q being sequence of ( the carrier of () *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )

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 T being DivSequence of A
for p being sequence of ((REAL n) *)
for q being sequence of ( the carrier of () *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )

let f be Function of A,(REAL n); :: thesis: for g being Function of A,()
for T being DivSequence of A
for p being sequence of ((REAL n) *)
for q being sequence of ( the carrier of () *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )

let g be Function of A,(); :: thesis: for T being DivSequence of A
for p being sequence of ((REAL n) *)
for q being sequence of ( the carrier of () *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )

let T be DivSequence of A; :: thesis: for p being sequence of ((REAL n) *)
for q being sequence of ( the carrier of () *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )

let p be sequence of ((REAL n) *); :: thesis: for q being sequence of ( the carrier of () *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )

let q be sequence of ( the carrier of () *); :: thesis: ( f = g & p = q implies ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T ) )
assume A1: ( f = g & p = q ) ; :: thesis: ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )
hereby :: thesis: ( q is middle_volume_Sequence of g,T implies p is middle_volume_Sequence of f,T )
assume A2: p is middle_volume_Sequence of f,T ; :: thesis: q is middle_volume_Sequence of g,T
for k being Element of NAT holds q . k is middle_volume of g,T . k
proof
let k be Element of NAT ; :: thesis: q . k is middle_volume of g,T . k
A3: p . k is middle_volume of f,T . k by ;
thus q . k is middle_volume of g,T . k by A1, A3, Th36; :: thesis: verum
end;
hence q is middle_volume_Sequence of g,T by INTEGR18:def 3; :: thesis: verum
end;
assume A4: q is middle_volume_Sequence of g,T ; :: thesis: p is middle_volume_Sequence of f,T
for k being Element of NAT holds p . k is middle_volume of f,T . k
proof
let k be Element of NAT ; :: thesis: p . k is middle_volume of f,T . k
A5: q . k is middle_volume of g,T . k by ;
thus p . k is middle_volume of f,T . k by A1, A5, Th36; :: thesis: verum
end;
hence p is middle_volume_Sequence of f,T by INTEGR15:def 7; :: thesis: verum