let p, q be FinSequence; :: thesis: ( ( p = p ^ q or p = q ^ p ) implies q = {} )
assume A1: ( p = p ^ q or p = q ^ p ) ; :: thesis: q = {}
( len (p ^ q) = (len p) + (len q) & len (q ^ p) = (len q) + (len p) & len p = (len p) + 0 ) by FINSEQ_1:35;
hence q = {} by A1; :: thesis: verum