theorem Th31: :: FINSEQ_1:31

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