theorem Th26: :: AFINSQ_1:28

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