theorem Th9: :: POLYFORM:11

for p, q, r being FinSequence holds len (p ^ q) <= len (p ^ (q ^ r))