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:21;
hence Seq ((f ^ g) | (dom f)) = (f ^ g) | (dom f) by FINSEQ_3:116; :: thesis: verum