theorem :: FINSEQ_1:102

for D being set
for f being b₁ -valued FinSequence holds f is FinSequence of D by LL;