theorem :: FINSEQ_1:75

for D being set
for p, q being b₁ -valued FinSequence holds p ^ q is FinSequence of D