theorem Th13: :: CALCUL_1:13

for Al being QC-alphabet
for f, g being FinSequence of CQC-WFF Al st 0 < len f holds
f is_Subsequence_of ((Ant f) ^ g) ^ <*(Suc f)*>