theorem Th10: :: FINSEQ_6:10

for f1, f2 being FinSequence holds f1 c= f1 ^ f2