let X be RealNormSpace; 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; 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; 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; 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; 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; ( ( 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 )
; 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 H1( Nat) -> Element of the carrier of X * = SS0 /. $1;
deffunc H2( 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) = H1(n) & S1 . ((2 * n) + 1) = H2(n) )
from INTEGR20:sch 1();
for i being Element of NAT holds S1 . i is middle_volume of h,T1 . i
then reconsider S1 = S1 as middle_volume_Sequence of h,T1 by INTEGR18:def 3;
take
S1
; for i being Nat holds
( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )
let i be Nat; ( 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; verum