let A be non empty closed_interval Subset of REAL; :: thesis: for T0, T being DivSequence of A ex T1 being DivSequence of A st
for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i )
let T0, T be DivSequence of A; :: thesis: ex T1 being DivSequence of A st
for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i )
A1: ( dom T0 = NAT & dom T = NAT ) by FUNCT_2:def 1;

now :: thesis: for i being object st i in NAT holds
T0 . i in REAL *

let i be object ; :: thesis: ( i in NAT implies T0 . i in REAL * )
assume i in NAT ; :: thesis: T0 . i in REAL *
then reconsider i1 = i as Nat ;
rng (T0 . i1) c= REAL ;
hence T0 . i in REAL * by FINSEQ_1:def 11; :: thesis: verum

end;

then reconsider S0 = T0 as sequence of (REAL *) by A1, FUNCT_2:3;

now :: thesis: for i being object st i in NAT holds
T . i in REAL *

let i be object ; :: thesis: ( i in NAT implies T . i in REAL * )
assume i in NAT ; :: thesis: T . i in REAL *
then reconsider i1 = i as Nat ;
rng (T . i1) c= REAL ;
hence T . i in REAL * by FINSEQ_1:def 11; :: thesis: verum

end;

then reconsider S = T as sequence of (REAL *) by A1, FUNCT_2:3;
deffunc H₁( Nat) -> Element of REAL * = S0 /. $1;
deffunc H₂( Nat) -> Element of REAL * = S /. $1;
consider T1 being sequence of (REAL *) such that
A2: for n being Nat holds
( T1 . (2 * n) = H₁(n) & T1 . ((2 * n) + 1) = H₂(n) ) from INTEGR20:sch 1();
A3: dom T1 = NAT by FUNCT_2:def 1;

now :: thesis: for i being object st i in NAT holds
T1 . i in divs A

let i be object ; :: thesis: ( i in NAT implies T1 . b₁ in divs A )
assume i in NAT ; :: thesis: T1 . b₁ in divs A
then reconsider j = i as Nat ;
consider k being Nat such that
A4: ( j = 2 * k or j = (2 * k) + 1 ) by Th14;
reconsider k = k as Element of NAT by ORDINAL1:def 12;

per cases ( j = 2 * k or j = (2 * k) + 1 ) by A4;

suppose j = 2 * k ; :: thesis: T1 . b₁ in divs A

then T1 . j = S0 /. k by A2
.= T0 . k ;
hence T1 . i in divs A by INTEGRA1:def 3; :: thesis: verum

end;

suppose j = (2 * k) + 1 ; :: thesis: T1 . b₁ in divs A

then T1 . j = S /. k by A2
.= T . k ;
hence T1 . i in divs A by INTEGRA1:def 3; :: thesis: verum

end;

end;

end;

then reconsider T1 = T1 as DivSequence of A by A3, FUNCT_2:3;
take T1 ; :: thesis: for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i )
let i be Nat; :: thesis: ( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i )
i in NAT by ORDINAL1:def 12;
then A5: ( i in dom S0 & i in dom S ) by FUNCT_2:def 1;
A6: T1 . (2 * i) = S0 /. i by A2
.= T0 . i by A5, PARTFUN1:def 6 ;
T1 . ((2 * i) + 1) = S /. i by A2
.= T . i by A5, PARTFUN1:def 6 ;
hence ( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) by A6; :: thesis: verum