let g, f be FinSequence of CQC-WFF ; :: thesis: dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f
rng (Sgm (seq ((len g),(len f)))) = seq ((len g),(len f)) by Th12;
then A1: rng (Sgm (seq ((len g),(len f)))) c= dom (g ^ f) by Th14;
dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom ((Sgm (seq ((len g),(len f)))) * (g ^ f)) by Th16;
then dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom (Sgm (seq ((len g),(len f)))) by A1, RELAT_1:27;
hence dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f by Th11; :: thesis: verum