theorem Th1: :: CALCUL_1:1

for Al being QC-alphabet
for f, g being FinSequence of CQC-WFF Al st f is_Subsequence_of g holds
( rng f c= rng g & ex N being Subset of NAT st rng f c= rng (g | N) )