for A being set
for i being Element of NAT
for p being FinSequence of A holds
( p in i -tuples_on A iff len p = i )