theorem :: AFINSQ_1:31

for p, q being XFinSequence
for D being set st p ^ q is XFinSequence of D holds
( p is XFinSequence of D & q is XFinSequence of D )