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:46;
hence dom (Seq ((g ^ f) | (seq (len g),(len f)))) = dom f by Th11; :: thesis: verum