theorem Th29: :: FINSEQ_1:29

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