:: deftheorem Def2 defines Set_Sequence MEASURE8:def 2 :
for X being set
for F being Field_Subset of X
for b₃ being SetSequence of X holds
( b₃ is Set_Sequence of F iff for n being Nat holds b₃ . n in F );