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