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 )

for k being Element of NAT holds p . k is middle_volume of f,T . k

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 A4:
q is middle_volume_Sequence of g,T
; :: thesis: p is middle_volume_Sequence of f,Tassume 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

end;for k being Element of NAT holds q . k is middle_volume of g,T . k

proof

hence
q is middle_volume_Sequence of g,T
by INTEGR18:def 3; :: thesis: verum
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;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

for k being Element of NAT holds p . k is middle_volume of f,T . k

proof

hence
p is middle_volume_Sequence of f,T
by INTEGR15:def 7; :: thesis: verum
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;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