theorem Th27: :: AFINSQ_1:30

for p, q being XFinSequence st p ^ q = {} holds
( p = {} & q = {} )