theorem Th16: :: POLYFORM:18

for x being object
for p, q being FinSequence holds ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x