for p, q being FinSequence holds rng p c= rng (p ^ q)