for A, x being set
for m being Nat st x in m -tuples_on A holds
x is FinSequence of A