theorem Th1: :: POLNOT_1:1

for p, q, r, s being FinSequence st p ^ q = r ^ s holds
ex t being FinSequence st
( p ^ t = r or p = r ^ t )