theorem Th14: :: POLYFORM:16

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