let f, g be FinSequence of CQC-WFF ; :: thesis: Seq ((f ^ g) | (dom f)) = (f ^ g) | (dom f)
(f ^ g) | (dom f) = f by FINSEQ_1:33;
hence Seq ((f ^ g) | (dom f)) = (f ^ g) | (dom f) by FINSEQ_3:125; :: thesis: verum