theorem Th56: :: FINSEQ_3:58

for p, q being FinSequence
for A being set holds p " A c= (p ^ q) " A