:: deftheorem Def5 defines -xtuples_of HILB10_2:def 5 :
for D being non empty set
for n being Nat
for b₃ being Subset of (D ^omega) holds
( b₃ = n -xtuples_of D iff for x being object holds
( x in b₃ iff x is b₂ -element XFinSequence of D ) );