theorem Th16: :: INTEGR20:16

for A being non empty closed_interval Subset of REAL
for T0, T, T1 being DivSequence of A st delta T0 is convergent & lim (delta T0) = 0 & delta T is convergent & lim (delta T) = 0 & ( for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) holds
( delta T1 is convergent & lim (delta T1) = 0 )