theorem Th8: :: CALCUL_1:8

for Al being QC-alphabet
for f, g being FinSequence of CQC-WFF Al holds f is_Subsequence_of f ^ g