theorem :: FINSEQ_2:141

for i being natural Number
for A being set
for x being object st x in i -tuples_on A holds
x is b₁ -element FinSequence by Lm7;