for p being FinSequence holds p - (rng p) = {} by Th66;