for p, q being XFinSequence holds len (p ^ q) = (len p) + (len q) by Def3;