for r being Real
for p, q being FinSequence of REAL holds len ((p ^ <*r*>) ^ q) = ((len p) + (len q)) + 1