let A be non empty closed_interval Subset of REAL; :: thesis:
let rho be Function of A,REAL; :: thesis:
let u be PartFunc of REAL,REAL; :: thesis:
let T0, T, T1 be DivSequence of A; :: thesis:
let S0 be middle_volume_Sequence of rho,u,T0; :: thesis:
let S be middle_volume_Sequence of rho,u,T; :: thesis:
assume A2: 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 (REAL *) ;
deffunc H₁( Nat) -> Element of REAL * = In ((SS0 . $1),(REAL *));
deffunc H₂( Nat) -> Element of REAL * = In ((SS . $1),(REAL *));
consider S1 being sequence of (REAL *) such that
A3: 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 rho,u,T1 . i

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

then S1 . i = In ((SS0 . k),(REAL *)) by A3
.= S0 . k by FUNCT_2:5, SUBSET_1:def 8 ;
hence S1 . i is middle_volume of rho,u,T1 . i by A2, A5; :: thesis:

end;

then S1 . i = In ((SS . k),(REAL *)) by A3
.= S . k by FUNCT_2:5, SUBSET_1:def 8 ;
hence S1 . i is middle_volume of rho,u,T1 . i by A2, A6; :: thesis:

end;

then reconsider S1 = S1 as middle_volume_Sequence of rho,u,T1 by INTEGR22:def 6;
take S1 ; :: thesis:
let i be Nat; :: thesis:
A7: i is Element of NAT by ORDINAL1:def 12;
A8: S1 . (2 * i) = In ((SS0 . i),(REAL *)) by A3
.= S0 . i by A7, FUNCT_2:5, SUBSET_1:def 8 ;
S1 . ((2 * i) + 1) = In ((SS . i),(REAL *)) by A3
.= S . i by A7, FUNCT_2:5, SUBSET_1:def 8 ;
hence ( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i ) by A8; :: thesis: