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 p being sequence of ((REAL n) *)
for q being sequence of ( the carrier of (REAL-NS n) *) 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,(REAL-NS n)
for T being DivSequence of A
for p being sequence of ((REAL n) *)
for q being sequence of ( the carrier of (REAL-NS n) *) 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,(REAL-NS n)
for T being DivSequence of A
for p being sequence of ((REAL n) *)
for q being sequence of ( the carrier of (REAL-NS n) *) 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,(REAL-NS n); :: thesis: for T being DivSequence of A
for p being sequence of ((REAL n) *)
for q being sequence of ( the carrier of (REAL-NS n) *) 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 (REAL-NS n) *) 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 (REAL-NS n) *) 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 (REAL-NS n) *); :: 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 A2, INTEGR15:def 7;
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 A4, INTEGR18:def 3;
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