theorem Th16: :: FINSEQ_6:142

for p, q being FinSequence st 1 < len q holds
(p ^' q) . (len (p ^' q)) = q . (len q)