for f, g being FinSequence holds len f <= len (f ^' g)