:: deftheorem Def8 defines doms HILB10_7:def 8 :
for F being FinSequence-yielding FinSequence
for b₂ being finite Subset of (NAT *) holds
( b₂ = doms F iff for x being object holds
( x in b₂ iff ex p being FinSequence st
( p = x & len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) ) );