theorem Th16: :: FOMODEL0:16

for Y being set
for m being Nat
for p being FinSequence st p is Y -valued & p is m -element holds
p in m -tuples_on Y