theorem Th35: :: FINSEQ_1:35

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