:: deftheorem Def1 defines IntervalSequence COUSIN:def 1 :
for a, b being Real_Sequence
for b₃ being SetSequence of (REAL 1) holds
( b₃ = IntervalSequence (a,b) iff for i being Nat holds b₃ . i = product <*[.(a . i),(b . i).]*> );