theorem Th16: :: COUSIN:23

for a, b being Real_Sequence
for i being Nat holds (IntervalSequence (a,b)) . i = product <*[.(a . i),(b . i).]*>