:: deftheorem Def1 defines FinSequence MEASURE8:def 1 :
for X being set
for F being Field_Subset of X
for b₃ being FinSequence of bool X holds
( b₃ is FinSequence of F iff for k being Nat st k in dom b₃ holds
b₃ . k in F );