let f, g be FinSequence of CQC-WFF ; :: 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:19;
A1: N = dom f by FINSEQ_1:def 3;
then f c= f1 by FINSEQ_1:33;
hence f c= Seq ((f ^ g) | N) by A1, Th7; :: thesis: verum