theorem Th30: :: FINSEQ_1:30

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