theorem Th17: :: FINSEQ_6:143

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