for p, q, r being XFinSequence st ( p ^ r = q ^ r or r ^ p = r ^ q ) holds
p = q