let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al holds f is_Subsequence_of f ^ g
let f, g be FinSequence of CQC-WFF Al; :: thesis: f is_Subsequence_of f ^ g
set a = len f;
take N = Seg (len f); :: according to CALCUL_1:def 4 :: thesis: f c= Seq ((f ^ g) | N)
reconsider f1 = (f ^ g) | N as FinSequence by FINSEQ_1:15;
A1: N = dom f by FINSEQ_1:def 3;
then f c= f1 by FINSEQ_1:21;
hence f c= Seq ((f ^ g) | N) by A1, Th7; :: thesis: verum