theorem Th130: :: FINSEQ_2:132

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