let X be RealNormSpace; :: thesis:
let A be non empty closed_interval Subset of REAL; :: thesis:
let h be Function of A, the carrier of X; :: thesis:
let T0, T, T1 be DivSequence of A; :: thesis:
let S0 be middle_volume_Sequence of h,T0; :: thesis:
let S be middle_volume_Sequence of h,T; :: thesis:
assume A1: for k being Nat holds
( T1 . (2 * k) = T0 . k & T1 . ((2 * k) + 1) = T . k ) ; :: thesis:
reconsider SS0 = S0, SS = S as sequence of ( the carrier of X *) ;
deffunc H₁( Nat) -> Element of the carrier of X * = SS0 /. $1;
deffunc H₂( Nat) -> Element of the carrier of X * = SS /. $1;
consider S1 being sequence of ( the carrier of X *) such that
A2: for n being Nat holds
( S1 . (2 * n) = H₁(n) & S1 . ((2 * n) + 1) = H₂(n) ) from INTEGR20:sch 1();
for i being Element of NAT holds S1 . i is middle_volume of h,T1 . i

proof

let i be Element of NAT ; :: thesis:
consider k being Nat such that
A3: ( i = 2 * k or i = (2 * k) + 1 ) by Th14;
reconsider k = k as Element of NAT by ORDINAL1:def 12;

per cases by A3;

suppose A4: i = 2 * k ; :: thesis:

then S1 . i = SS0 /. k by A2
.= S0 . k ;
hence S1 . i is middle_volume of h,T1 . i by A4, A1; :: thesis:

end;

suppose A5: i = (2 * k) + 1 ; :: thesis:

then S1 . i = SS /. k by A2
.= S . k ;
hence S1 . i is middle_volume of h,T1 . i by A5, A1; :: thesis:

end;

end;

end;

then reconsider S1 = S1 as middle_volume_Sequence of h,T1 by INTEGR18:def 3;
take S1 ; :: thesis:
let i be Nat; :: thesis:
i in NAT by ORDINAL1:def 12;
then A6: ( i in dom SS0 & i in dom SS ) by FUNCT_2:def 1;
A7: S1 . (2 * i) = SS0 /. i by A2
.= S0 . i by PARTFUN1:def 6, A6 ;
S1 . ((2 * i) + 1) = SS /. i by A2
.= S . i by PARTFUN1:def 6, A6 ;
hence ( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i ) by A7; :: thesis: