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