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

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