for A being non empty closed_interval Subset of REAL
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 )