theorem :: FINSEQ_1:75

for D being set
for p, q being FinSequence of D holds p ^ q is FinSequence of D ;