theorem :: FINSEQ_1:88

for x being object
for p, q being FinSequence holds
( not p ^ q = <*x*> or ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) )