let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al holds Seq ((f ^ g) | (dom f)) = (f ^ g) | (dom f)
let f, g be FinSequence of CQC-WFF Al; :: thesis: Seq ((f ^ g) | (dom f)) = (f ^ g) | (dom f)
(f ^ g) | (dom f) = f by FINSEQ_1:21;
hence Seq ((f ^ g) | (dom f)) = (f ^ g) | (dom f) by FINSEQ_3:116; :: thesis: verum