theorem :: FINSEQ_1:87

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