let X be RealNormSpace; :: thesis: for A being non empty closed_interval Subset of REAL
for h being Function of A, the carrier of X
for T0, T, T1 being DivSequence of A
for S0 being middle_volume_Sequence of h,T0
for S being middle_volume_Sequence of h,T st ( for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) holds
ex S1 being middle_volume_Sequence of h,T1 st
for i being Nat holds
( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )
let A be non empty closed_interval Subset of REAL; :: thesis: for h being Function of A, the carrier of X
for T0, T, T1 being DivSequence of A
for S0 being middle_volume_Sequence of h,T0
for S being middle_volume_Sequence of h,T st ( for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) holds
ex S1 being middle_volume_Sequence of h,T1 st
for i being Nat holds
( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )
let h be Function of A, the carrier of X; :: thesis: for T0, T, T1 being DivSequence of A
for S0 being middle_volume_Sequence of h,T0
for S being middle_volume_Sequence of h,T st ( for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) holds
ex S1 being middle_volume_Sequence of h,T1 st
for i being Nat holds
( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )
let T0, T, T1 be DivSequence of A; :: thesis: for S0 being middle_volume_Sequence of h,T0
for S being middle_volume_Sequence of h,T st ( for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) holds
ex S1 being middle_volume_Sequence of h,T1 st
for i being Nat holds
( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )
let S0 be middle_volume_Sequence of h,T0; :: thesis: for S being middle_volume_Sequence of h,T st ( for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) holds
ex S1 being middle_volume_Sequence of h,T1 st
for i being Nat holds
( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )
let S be middle_volume_Sequence of h,T; :: thesis: ( ( for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) implies ex S1 being middle_volume_Sequence of h,T1 st
for i being Nat holds
( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i ) )
assume A1: for k being Nat holds
( T1 . (2 * k) = T0 . k & T1 . ((2 * k) + 1) = T . k ) ; :: thesis: ex S1 being middle_volume_Sequence of h,T1 st
for i being Nat holds
( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )
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: S1 . i is middle_volume of h,T1 . i
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 ( i = 2 * k or i = (2 * k) + 1 ) by A3;

suppose A4: i = 2 * k ; :: thesis: S1 . i is middle_volume of h,T1 . i

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

end;

suppose A5: i = (2 * k) + 1 ; :: thesis: S1 . i is middle_volume of h,T1 . i

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

end;

end;

end;

then reconsider S1 = S1 as middle_volume_Sequence of h,T1 by INTEGR18:def 3;
take S1 ; :: thesis: for i being Nat holds
( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )
let i be Nat; :: thesis: ( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )
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: verum