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) ) by Th22;
hence q = {} by A1; :: thesis: verum