theorem :: FINSEQ_2:133

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